awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Sl2
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_1 : IsSl2Triple h e f
x y u_1 : L
hu : Membership.mem (γ := Set L) {e, f, h} u_1
t : R
u : L
hv : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u
hv' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u_1, u⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u_1, t • u⁆

Tactic:
simpa only [lie_smul] using smul_mem _ t hv'

Premises used: lie_smul, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.Sl2
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
⊢ u = e ∨ u = f ∨ u = h

Tactic:
push _ ∈ _ at hu hv
-- Module: Mathlib.Algebra.Lie.Sl2
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
⊢ v = e ∨ v = f ∨ v = h

Tactic:
push _ ∈ _ at hu hv
-- Module: Mathlib.Algebra.Lie.Sl2
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⁆
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⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆

Tactic:
rcases hu with rfl | rfl | rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Sl2
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⁆
mem₂ : ∀ (t : IsSl2Triple v u f), Membership.mem (γ := Submodule R L) (span R {u, f, v}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, h}) ⁅u, v⁆

Tactic:
rcases hv with rfl | rfl | rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Sl2
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⁆
mem₂ : ∀ (t : IsSl2Triple v e u), Membership.mem (γ := Submodule R L) (span R {e, u, v}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, h}) ⁅u, v⁆

Tactic:
rcases hv with rfl | rfl | rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Sl2
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
mem : ∀ (t : IsSl2Triple u v f), Membership.mem (γ := Submodule R L) (span R {v, f, u}) ⁅u, v⁆
mem₁ : ∀ (t : IsSl2Triple u e v), Membership.mem (γ := Submodule R L) (span R {e, v, u}) ⁅u, v⁆
mem₂ : ∀ (t : IsSl2Triple v e f), Membership.mem (γ := Submodule R L) (span R {e, f, v}) ⁅v, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, u}) ⁅u, v⁆

Tactic:
rcases hv with rfl | rfl | rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Sl2
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 v : L
t : IsSl2Triple h v f
__spread.0 : Submodule R L := span R {v, f, h}
⊢ Membership.mem (γ := Submodule R L) (span R {v, f, h}) ⁅v, v⁆

Tactic:
simp only [lie_self, zero_mem]

Premises used: lie_self, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Sl2
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 v : L
t : IsSl2Triple h v f
__spread.0 : Submodule R L := span R {v, f, h}
⊢ Membership.mem (γ := Submodule R L) (span R {v, f, h}) ⁅v, v⁆

Tactic:
try simp only [lie_self, zero_mem]

Premises used: lie_self, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Sl2
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 v : L
t : IsSl2Triple h e v
__spread.0 : Submodule R L := span R {e, v, h}
⊢ Membership.mem (γ := Submodule R L) (span R {e, v, h}) ⁅v, v⁆

Tactic:
simp only [lie_self, zero_mem]

Premises used: lie_self, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Sl2
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 v : L
t : IsSl2Triple h e v
__spread.0 : Submodule R L := span R {e, v, h}
⊢ Membership.mem (γ := Submodule R L) (span R {e, v, h}) ⁅v, v⁆

Tactic:
try simp only [lie_self, zero_mem]

Premises used: lie_self, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Sl2
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 v : L
t : IsSl2Triple v e f
__spread.0 : Submodule R L := span R {e, f, v}
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, v}) ⁅v, v⁆

Tactic:
simp only [lie_self, zero_mem]

Premises used: lie_self, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Sl2
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 v : L
t : IsSl2Triple v e f
__spread.0 : Submodule R L := span R {e, f, v}
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, v}) ⁅v, v⁆

Tactic:
try simp only [lie_self, zero_mem]

Premises used: lie_self, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple h u v
__spread.0 : Submodule R L := span R {u, v, h}
mem : Membership.mem (γ := Submodule R L) (span R {u, v, h}) h
⊢ Membership.mem (γ := Submodule R L) (span R {u, v, h}) ⁅u, v⁆

Tactic:
rw [t.lie_e_f]

Premises used: IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple h u v
__spread.0 : Submodule R L := span R {u, v, h}
mem : Membership.mem (γ := Set L) {u, v, h} h
⊢ Membership.mem (γ := Submodule R L) (span R {u, v, h}) h

Tactic:
apply subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple h u v
__spread.0 : Submodule R L := span R {u, v, h}
⊢ Membership.mem (γ := Set L) {u, v, h} h

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
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
f x y u v : L
t : IsSl2Triple v u f
__spread.0 : Submodule R L := span R {u, f, v}
mem : Membership.mem (γ := Submodule R L) (span R {u, f, v}) (HSMul.hSMul (α := ℕ) 2 u)
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, v}) ⁅u, v⁆

Tactic:
rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]

Premises used: neg_mem_iff, lie_skew, IsSl2Triple.lie_h_e_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
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
f x y u v : L
t : IsSl2Triple v u f
__spread.0 : Submodule R L := span R {u, f, v}
apply : Membership.mem (γ := Set L) {u, f, v} u
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, v}) (HSMul.hSMul (α := ℕ) 2 u)

Tactic:
apply nsmul_mem <| subset_span _

Premises used: nsmul_mem, Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.Sl2
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
f x y u v : L
t : IsSl2Triple v u f
__spread.0 : Submodule R L := span R {u, f, v}
⊢ Membership.mem (γ := Set L) {u, f, v} u

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple h v u
__spread.0 : Submodule R L := span R {v, u, h}
mem : Membership.mem (γ := Submodule R L) (span R {v, u, h}) h
⊢ Membership.mem (γ := Submodule R L) (span R {v, u, h}) ⁅u, v⁆

Tactic:
rw [← lie_skew, t.lie_e_f, neg_mem_iff]

Premises used: neg_mem_iff, lie_skew, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple h v u
__spread.0 : Submodule R L := span R {v, u, h}
mem : Membership.mem (γ := Set L) {v, u, h} h
⊢ Membership.mem (γ := Submodule R L) (span R {v, u, h}) h

Tactic:
apply subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple h v u
__spread.0 : Submodule R L := span R {v, u, h}
⊢ Membership.mem (γ := Set L) {v, u, h} h

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple v e u
__spread.0 : Submodule R L := span R {e, u, v}
mem : Membership.mem (γ := Submodule R L) (span R {e, u, v}) (HSMul.hSMul (α := ℕ) 2 u)
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, v}) ⁅u, v⁆

Tactic:
rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]

Premises used: neg_neg, lie_skew, IsSl2Triple.lie_h_f_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple v e u
__spread.0 : Submodule R L := span R {e, u, v}
apply : Membership.mem (γ := Set L) {e, u, v} u
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, v}) (HSMul.hSMul (α := ℕ) 2 u)

Tactic:
apply nsmul_mem <| subset_span _

Premises used: nsmul_mem, Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple v e u
__spread.0 : Submodule R L := span R {e, u, v}
⊢ Membership.mem (γ := Set L) {e, u, v} u

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
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
f x y u v : L
t : IsSl2Triple u v f
__spread.0 : Submodule R L := span R {v, f, u}
mem : Membership.mem (γ := Submodule R L) (span R {v, f, u}) (HSMul.hSMul (α := ℕ) 2 v)
⊢ Membership.mem (γ := Submodule R L) (span R {v, f, u}) ⁅u, v⁆

Tactic:
rw [t.lie_h_e_nsmul]

Premises used: IsSl2Triple.lie_h_e_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
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
f x y u v : L
t : IsSl2Triple u v f
__spread.0 : Submodule R L := span R {v, f, u}
apply : Membership.mem (γ := Set L) {v, f, u} v
⊢ Membership.mem (γ := Submodule R L) (span R {v, f, u}) (HSMul.hSMul (α := ℕ) 2 v)

Tactic:
apply nsmul_mem <| subset_span _

Premises used: nsmul_mem, Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.Sl2
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
f x y u v : L
t : IsSl2Triple u v f
__spread.0 : Submodule R L := span R {v, f, u}
⊢ Membership.mem (γ := Set L) {v, f, u} v

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple u e v
__spread.0 : Submodule R L := span R {e, v, u}
mem : Membership.mem (γ := Submodule R L) (span R {e, v, u}) (HSMul.hSMul (α := ℕ) 2 v)
⊢ Membership.mem (γ := Submodule R L) (span R {e, v, u}) ⁅u, v⁆

Tactic:
rw [t.lie_h_f_nsmul, neg_mem_iff]

Premises used: neg_mem_iff, IsSl2Triple.lie_h_f_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple u e v
__spread.0 : Submodule R L := span R {e, v, u}
apply : Membership.mem (γ := Set L) {e, v, u} v
⊢ Membership.mem (γ := Submodule R L) (span R {e, v, u}) (HSMul.hSMul (α := ℕ) 2 v)

Tactic:
apply nsmul_mem <| subset_span _

Premises used: nsmul_mem, Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.Sl2
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 x y u v : L
t : IsSl2Triple u e v
__spread.0 : Submodule R L := span R {e, v, u}
⊢ Membership.mem (γ := Set L) {e, v, u} v

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
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
hy : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
u : L
hu : Membership.mem (γ := Set L) {e, f, h} u
mem : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, 0⁆
mem₁ :
  ∀ (u_1 v : L) (hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u_1)
    (hv : Membership.mem (γ := Submodule R L) (span R {e, f, h}) v)
    (hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, u_1⁆)
    (hv' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, u_1 + v⁆
mem₂ :
  ∀ (t : R) (u_1 : L) (hv : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u_1)
    (hv' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, u_1⁆),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, t • u_1⁆
mem₃ :
  ∀ (v : L) (hv : Membership.mem (γ := Set L) {e, f, h} v),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆

Tactic:
induction hy using span_induction with
      | zero => simp
      | add u v hu hv hu' hv' => simpa only [lie_add] using add_mem hu' hv'
      | smul t u hv hv' => simpa only [lie_smul] using smul_mem _ t hv'
      | mem v hv =>
        push _ ∈ _ at hu hv
        rcases hu with rfl | rfl | rfl <;>
        rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])
        · rw [t.lie_e_f]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp
        · rw [← lie_skew, t.lie_e_f, neg_mem_iff]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_e_nsmul]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_f_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp

Premises used: neg_mem_iff, lie_smul, nsmul_mem, neg_neg, lie_self, lie_skew, Submodule.smul, IsSl2Triple.lie_h_f_nsmul, Submodule.zero, IsSl2Triple.lie_h_e_nsmul, ZeroMemClass.zero_mem, Submodule.subset_span, Submodule.add, IsSl2Triple.lie_e_f, rfl, lie_add
-- Module: Mathlib.Algebra.Lie.Sl2
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 (γ := Submodule R L) (span R {e, f, h}) x
hy : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
zero : Membership.mem (γ := Submodule R L) (span R {e, f, h}) (Bracket.bracket (L := L) 0 y)
add :
  ∀ (u v : L) (hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u)
    (hv : Membership.mem (γ := Submodule R L) (span R {e, f, h}) v)
    (hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆)
    (hv' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅v, y⁆),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u + v, y⁆
smul :
  ∀ (t : R) (u : L) (hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u)
    (hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅t • u, y⁆
mem :
  ∀ (u : L) (hu : Membership.mem (γ := Set L) {e, f, h} u),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅x, y⁆

Tactic:
induction hx using span_induction with
    | zero => simp
    | add u v hu hv hu' hv' => simpa only [add_lie] using add_mem hu' hv'
    | smul t u hu hu' => simpa only [smul_lie] using smul_mem _ t hu'
    | mem u hu =>
      induction hy using span_induction with
      | zero => simp
      | add u v hu hv hu' hv' => simpa only [lie_add] using add_mem hu' hv'
      | smul t u hv hv' => simpa only [lie_smul] using smul_mem _ t hv'
      | mem v hv =>
        push _ ∈ _ at hu hv
        rcases hu with rfl | rfl | rfl <;>
        rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])
        · rw [t.lie_e_f]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp
        · rw [← lie_skew, t.lie_e_f, neg_mem_iff]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_e_nsmul]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_f_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp

Premises used: neg_mem_iff, lie_smul, nsmul_mem, neg_neg, lie_self, lie_skew, smul_lie, Submodule.smul, IsSl2Triple.lie_h_f_nsmul, Submodule.zero, IsSl2Triple.lie_h_e_nsmul, ZeroMemClass.zero_mem, Submodule.subset_span, Submodule.add, IsSl2Triple.lie_e_f, rfl, lie_add, add_lie
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
simp_rw :
  Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
simp_rw₁ :
  Membership.mem (γ := LieSubalgebra R L) { toSubmodule := Submodule.span R {e, f, h}, lie_mem' := ⋯ } x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
simp_rw₂ :
  Membership.mem (γ := Submodule R L) (Submodule.span R {e, f, h}) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
simp_rw₃ :
  (∃ (a : R) (b : R) (c : R), a • e + b • f + c • h = x) ↔ ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
⊢ Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple,
    eq_comm]

Premises used: LieSubalgebra.mem_toSubmodule, IsSl2Triple.toLieSubalgebra, eq_comm, Submodule.mem_span_triple, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Sl2
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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
⊢ Eq (α := M)
    (⁅f,
        (HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m⁆ :
      M)
    ((HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)

Tactic:
simp [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Lie.Sl2
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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
⊢ ⁅h,
      (HPow.hPow (α := End R M) (β := ℕ)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) 0 :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑0 : R))
      ((HPow.hPow (α := End R M) (β := ℕ)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) 0 :
            (a : M) → M)
          m :
        M)

Tactic:
simpa using P.lie_h

Premises used: IsSl2Triple.HasPrimitiveVectorWith.lie_h