Theorems / mh_alge_c62440

Mathlib held-out

Algebra · hard

Statement, exactly as the model and Lean see it
theorem lg_target {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) : i.range = LieIdeal.toLieSubalgebra R L p.ker ↔ Function.Exact ⇑i ⇑p := by
Mathlib declaration
LieHom.range_eq_ker_iff
Held-out module
Mathlib.Algebra.Lie.Extension
Banned modules (itself + downstream)
2
Reference proof premises (reachable / held-out)
4 / 0

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00033

Attempts

  1. sample 0 · round 0Syntax error13.3 s model time
    Proof
    intro h
split
· intro H
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L i.range
  haveI : IsLieSubalgebra R (p.ker) := by exact LieIdeal.toLieSubalgebra.isLieSubalgebra R L p.ker
  haveI : IsLieSubalgebra R (i.range......
    What Lean printed (this is all the model sees on repair)
    24:41: error: unexpected token '...'; expected term

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

lemma _root_.LieHom.range_eq_ker_iff (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) :
    i.range = p.ker ↔ Exact i p :=
  ⟨fun h x ↦ by simp [← LieHom.coe_range, h], fun h ↦ (p.ker.toLieSubalgebra.ext i.range h).symm⟩