awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A
have mp : Aᵀ * u • J = u • J * -A → Aᵀ * J = J * -A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
u : Rˣ
J A : Matrix n n R
mp : Aᵀ * u • J = u • J * -A → Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A
have mpr : Aᵀ * J = J * -A → Aᵀ * u • J = u • J * -A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅f, e⁆ = -h
have rw : -⁅f, e⁆ = h
Tactic: rw [← neg_eq_iff_eq_neg, lie_skew, ht.lie_e_f]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅f, e⁆ = h
⊢ ⁅f, e⁆ = -h
have rw₁ : ⁅e, f⁆ = h
Tactic: rw [← neg_eq_iff_eq_neg, lie_skew, ht.lie_e_f]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅f, e⁆ = h
rw₁ : ⁅e, f⁆ = h
⊢ ⁅f, e⁆ = -h
have rw₂ : h = h
Tactic: rw [← neg_eq_iff_eq_neg, lie_skew, ht.lie_e_f]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅-h, f⁆ = HSMul.hSMul (α := ℕ) 2 f
have rw : -⁅h, f⁆ = HSMul.hSMul (α := ℕ) 2 f
Tactic: rw [neg_lie, neg_eq_iff_eq_neg, ht.lie_h_f_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅h, f⁆ = HSMul.hSMul (α := ℕ) 2 f
⊢ ⁅-h, f⁆ = HSMul.hSMul (α := ℕ) 2 f
have rw₁ : ⁅h, f⁆ = -HSMul.hSMul (α := ℕ) 2 f
Tactic: rw [neg_lie, neg_eq_iff_eq_neg, ht.lie_h_f_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅h, f⁆ = HSMul.hSMul (α := ℕ) 2 f
rw₁ : ⁅h, f⁆ = -HSMul.hSMul (α := ℕ) 2 f
⊢ ⁅-h, f⁆ = HSMul.hSMul (α := ℕ) 2 f
have rw₂ : -HSMul.hSMul (α := ℕ) 2 f = -HSMul.hSMul (α := ℕ) 2 f
Tactic: rw [neg_lie, neg_eq_iff_eq_neg, ht.lie_h_f_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅-h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e
have rw : -⁅h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e
Tactic: rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅-h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e
have rw₁ : ⁅h, e⁆ = HSMul.hSMul (α := ℕ) 2 e
Tactic: rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e
rw₁ : ⁅h, e⁆ = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅-h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e
have rw₂ : HSMul.hSMul (α := ℕ) 2 e = HSMul.hSMul (α := ℕ) 2 e
Tactic: rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
⊢ e ≠ 0
have this : h ≠ 0
Tactic: have := t.h_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ e ≠ 0
have contrapose : ∀ (this : e = 0), h = 0
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
⊢ f ≠ 0
have this : h ≠ 0
Tactic: have := t.h_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ f ≠ 0
have contrapose : ∀ (this : f = 0), h = 0
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ ⁅e, m⁆ = 0
have suffices : HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
Tactic: suffices 2 • ⁅e, m⁆ = 0 by simpa using this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₁ : ⁅⁅h, e⁆, m⁆ = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₆ : ρ • ⁅h, m⁆ - μ • ρ • m = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
rw₆ : ρ • ⁅h, m⁆ - μ • ρ • m = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₇ : ρ • μ • m - μ • ρ • m = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
rw₆ : ρ • ⁅h, m⁆ - μ • ρ • m = 0
rw₇ : ρ • μ • m - μ • ρ • m = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₈ : (ρ * μ) • m - μ • ρ • m = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
rw₆ : ρ • ⁅h, m⁆ - μ • ρ • m = 0
rw₇ : ρ • μ • m - μ • ρ • m = 0
rw₈ : (ρ * μ) • m - μ • ρ • m = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₉ : (ρ * μ) • m - (μ * ρ) • m = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
rw₆ : ρ • ⁅h, m⁆ - μ • ρ • m = 0
rw₇ : ρ • μ • m - μ • ρ • m = 0
rw₈ : (ρ * μ) • m - μ • ρ • m = 0
rw₉ : (ρ * μ) • m - (μ * ρ) • m = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₁₀ : (μ * ρ) • m - (μ * ρ) • m = 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
rw₆ : ρ • ⁅h, m⁆ - μ • ρ • m = 0
rw₇ : ρ • μ • m - μ • ρ • m = 0
rw₈ : (ρ * μ) • m - μ • ρ • m = 0
rw₉ : (ρ * μ) • m - (μ * ρ) • m = 0
rw₁₀ : (μ * ρ) • m - (μ * ρ) • m = 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
have rw₁₁ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) x
hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) y
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) ⁅x, y⁆
have hx₁ : Membership.mem (γ := Submodule R L) (span R {e, f, h}) x
Tactic: simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) x
hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) y
hx₁ : Membership.mem (γ := Submodule R L) (span R {e, f, h}) x
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) ⁅x, y⁆
have hy₁ : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
Tactic: simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u : L
hu : Membership.mem (γ := Set L) {e, f, h} u
v : L
hv : Membership.mem (γ := Set L) {e, f, h} v
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆
have hu₁ : u = e ∨ u = f ∨ u = h
Tactic: push _ ∈ _ at hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u : L
hu : Membership.mem (γ := Set L) {e, f, h} u
v : L
hv : Membership.mem (γ := Set L) {e, f, h} v
hu₁ : u = e ∨ u = f ∨ u = h
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆
have hv₁ : v = e ∨ v = f ∨ v = h
Tactic: push _ ∈ _ at hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u v : L
hu : u = e ∨ u = f ∨ u = h
hv : v = e ∨ v = f ∨ v = h
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆
have mem : ∀ (t : IsSl2Triple h u f) (hv : v = u ∨ v = f ∨ v = h), Membership.mem (γ := Submodule R L) (span R {u, f, h}) ⁅u, v⁆
Tactic: rcases hu with rfl | rfl | rfl
Cleared hypotheses: e, t, hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u v : L
hu : u = e ∨ u = f ∨ u = h
hv : v = e ∨ v = f ∨ v = h
mem :
  ∀ (t : IsSl2Triple h u f) (hv : v = u ∨ v = f ∨ v = h), Membership.mem (γ := Submodule R L) (span R {u, f, h}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆
have mem₁ : ∀ (t : IsSl2Triple h e u) (hv : v = e ∨ v = u ∨ v = h), Membership.mem (γ := Submodule R L) (span R {e, u, h}) ⁅u, v⁆
Tactic: rcases hu with rfl | rfl | rfl
Cleared hypotheses: f, t, hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u v : L
hu : u = e ∨ u = f ∨ u = h
hv : v = e ∨ v = f ∨ v = h
mem :
  ∀ (t : IsSl2Triple h u f) (hv : v = u ∨ v = f ∨ v = h), Membership.mem (γ := Submodule R L) (span R {u, f, h}) ⁅u, v⁆
mem₁ :
  ∀ (t : IsSl2Triple h e u) (hv : v = e ∨ v = u ∨ v = h), Membership.mem (γ := Submodule R L) (span R {e, u, h}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆
have mem₂ : ∀ (t : IsSl2Triple u e f) (hv : v = e ∨ v = f ∨ v = u), Membership.mem (γ := Submodule R L) (span R {e, f, u}) ⁅u, v⁆
Tactic: rcases hu with rfl | rfl | rfl
Cleared hypotheses: h, t, hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h f x y u v : L
t : IsSl2Triple h u f
__spread.0 : Submodule R L := span R {u, f, h}
hv : v = u ∨ v = f ∨ v = h
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, h}) ⁅u, v⁆
have mem : ∀ (t : IsSl2Triple h v f), Membership.mem (γ := Submodule R L) (span R {v, f, h}) ⁅v, v⁆
Tactic: rcases hv with rfl | rfl | rfl
Cleared hypotheses: u, t, __spread.0, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h f x y u v : L
t : IsSl2Triple h u f
__spread.0 : Submodule R L := span R {u, f, h}
hv : v = u ∨ v = f ∨ v = h
mem : ∀ (t : IsSl2Triple h v f), Membership.mem (γ := Submodule R L) (span R {v, f, h}) ⁅v, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, h}) ⁅u, v⁆
have mem₁ : ∀ (t : IsSl2Triple h u v), Membership.mem (γ := Submodule R L) (span R {u, v, h}) ⁅u, v⁆
Tactic: rcases hv with rfl | rfl | rfl
Cleared hypotheses: f, t, __spread.0, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h f x y u v : L
t : IsSl2Triple h u f
__spread.0 : Submodule R L := span R {u, f, h}
hv : v = u ∨ v = f ∨ v = h
mem : ∀ (t : IsSl2Triple h v f), Membership.mem (γ := Submodule R L) (span R {v, f, h}) ⁅v, v⁆
mem₁ : ∀ (t : IsSl2Triple h u v), Membership.mem (γ := Submodule R L) (span R {u, v, h}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, h}) ⁅u, v⁆
have mem₂ : ∀ (t : IsSl2Triple v u f), Membership.mem (γ := Submodule R L) (span R {u, f, v}) ⁅u, v⁆
Tactic: rcases hv with rfl | rfl | rfl
Cleared hypotheses: h, t, __spread.0, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e x y u v : L
t : IsSl2Triple h e u
__spread.0 : Submodule R L := span R {e, u, h}
hv : v = e ∨ v = u ∨ v = h
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, h}) ⁅u, v⁆
have mem : ∀ (t : IsSl2Triple h v u), Membership.mem (γ := Submodule R L) (span R {v, u, h}) ⁅u, v⁆
Tactic: rcases hv with rfl | rfl | rfl
Cleared hypotheses: e, t, __spread.0, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e x y u v : L
t : IsSl2Triple h e u
__spread.0 : Submodule R L := span R {e, u, h}
hv : v = e ∨ v = u ∨ v = h
mem : ∀ (t : IsSl2Triple h v u), Membership.mem (γ := Submodule R L) (span R {v, u, h}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, h}) ⁅u, v⁆
have mem₁ : ∀ (t : IsSl2Triple h e v), Membership.mem (γ := Submodule R L) (span R {e, v, h}) ⁅v, v⁆
Tactic: rcases hv with rfl | rfl | rfl
Cleared hypotheses: u, t, __spread.0, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e x y u v : L
t : IsSl2Triple h e u
__spread.0 : Submodule R L := span R {e, u, h}
hv : v = e ∨ v = u ∨ v = h
mem : ∀ (t : IsSl2Triple h v u), Membership.mem (γ := Submodule R L) (span R {v, u, h}) ⁅u, v⁆
mem₁ : ∀ (t : IsSl2Triple h e v), Membership.mem (γ := Submodule R L) (span R {e, v, h}) ⁅v, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, h}) ⁅u, v⁆
have mem₂ : ∀ (t : IsSl2Triple v e u), Membership.mem (γ := Submodule R L) (span R {e, u, v}) ⁅u, v⁆
Tactic: rcases hv with rfl | rfl | rfl
Cleared hypotheses: h, t, __spread.0, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
e f x y u v : L
t : IsSl2Triple u e f
__spread.0 : Submodule R L := span R {e, f, u}
hv : v = e ∨ v = f ∨ v = u
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, u}) ⁅u, v⁆
have mem : ∀ (t : IsSl2Triple u v f), Membership.mem (γ := Submodule R L) (span R {v, f, u}) ⁅u, v⁆
Tactic: rcases hv with rfl | rfl | rfl
Cleared hypotheses: e, t, __spread.0, hv