awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mem : ∀ (t : IsSl2Triple u v f), Membership.mem (γ := Submodule R L) (span R {v, f, u}) ⁅u, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, u}) ⁅u, v⁆
have mem₁ : ∀ (t : IsSl2Triple u e v), Membership.mem (γ := Submodule R L) (span R {e, v, u}) ⁅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
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⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, u}) ⁅u, v⁆
have mem₂ : ∀ (t : IsSl2Triple v e f), Membership.mem (γ := Submodule R L) (span R {e, f, v}) ⁅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 x y u v : L
t : IsSl2Triple h u v
__spread.0 : Submodule R L := span R {u, v, h}
⊢ Membership.mem (γ := Submodule R L) (span R {u, v, h}) ⁅u, v⁆
have mem : Membership.mem (γ := Submodule R L) (span R {u, v, h}) h
Tactic: rw [t.lie_e_f]
-- 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 x y u v : L
t : IsSl2Triple h u v
__spread.0 : Submodule R L := span R {u, v, h}
⊢ Membership.mem (γ := Submodule R L) (span R {u, v, h}) h
have mem : Membership.mem (γ := Set L) {u, v, h} h
Tactic: apply subset_span
-- 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
f x y u v : L
t : IsSl2Triple v u f
__spread.0 : Submodule R L := span R {u, f, v}
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, v}) ⁅u, v⁆
have mem : Membership.mem (γ := Submodule R L) (span R {u, f, v}) (HSMul.hSMul (α := ℕ) 2 u)
Tactic: rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
-- 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
f x y u v : L
t : IsSl2Triple v u f
__spread.0 : Submodule R L := span R {u, f, v}
⊢ Membership.mem (γ := Submodule R L) (span R {u, f, v}) (HSMul.hSMul (α := ℕ) 2 u)
have apply : Membership.mem (γ := Set L) {u, f, v} u
Tactic: apply nsmul_mem <| subset_span _
-- 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 x y u v : L
t : IsSl2Triple h v u
__spread.0 : Submodule R L := span R {v, u, h}
⊢ Membership.mem (γ := Submodule R L) (span R {v, u, h}) ⁅u, v⁆
have mem : Membership.mem (γ := Submodule R L) (span R {v, u, h}) h
Tactic: rw [← lie_skew, t.lie_e_f, neg_mem_iff]
-- 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 x y u v : L
t : IsSl2Triple h v u
__spread.0 : Submodule R L := span R {v, u, h}
⊢ Membership.mem (γ := Submodule R L) (span R {v, u, h}) h
have mem : Membership.mem (γ := Set L) {v, u, h} h
Tactic: apply subset_span
-- 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 x y u v : L
t : IsSl2Triple v e u
__spread.0 : Submodule R L := span R {e, u, v}
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, v}) ⁅u, v⁆
have mem : Membership.mem (γ := Submodule R L) (span R {e, u, v}) (HSMul.hSMul (α := ℕ) 2 u)
Tactic: rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
-- 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 x y u v : L
t : IsSl2Triple v e u
__spread.0 : Submodule R L := span R {e, u, v}
⊢ Membership.mem (γ := Submodule R L) (span R {e, u, v}) (HSMul.hSMul (α := ℕ) 2 u)
have apply : Membership.mem (γ := Set L) {e, u, v} u
Tactic: apply nsmul_mem <| subset_span _
-- 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
f x y u v : L
t : IsSl2Triple u v f
__spread.0 : Submodule R L := span R {v, f, u}
⊢ Membership.mem (γ := Submodule R L) (span R {v, f, u}) ⁅u, v⁆
have mem : Membership.mem (γ := Submodule R L) (span R {v, f, u}) (HSMul.hSMul (α := ℕ) 2 v)
Tactic: rw [t.lie_h_e_nsmul]
-- 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
f x y u v : L
t : IsSl2Triple u v f
__spread.0 : Submodule R L := span R {v, f, u}
⊢ Membership.mem (γ := Submodule R L) (span R {v, f, u}) (HSMul.hSMul (α := ℕ) 2 v)
have apply : Membership.mem (γ := Set L) {v, f, u} v
Tactic: apply nsmul_mem <| subset_span _
-- 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 x y u v : L
t : IsSl2Triple u e v
__spread.0 : Submodule R L := span R {e, v, u}
⊢ Membership.mem (γ := Submodule R L) (span R {e, v, u}) ⁅u, v⁆
have mem : Membership.mem (γ := Submodule R L) (span R {e, v, u}) (HSMul.hSMul (α := ℕ) 2 v)
Tactic: rw [t.lie_h_f_nsmul, neg_mem_iff]
-- 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 x y u v : L
t : IsSl2Triple u e v
__spread.0 : Submodule R L := span R {e, v, u}
⊢ Membership.mem (γ := Submodule R L) (span R {e, v, u}) (HSMul.hSMul (α := ℕ) 2 v)
have apply : Membership.mem (γ := Set L) {e, v, u} v
Tactic: apply nsmul_mem <| subset_span _
-- 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 : L
hy : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
u : L
hu : Membership.mem (γ := Set L) {e, f, h} u
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
have mem : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, 0⁆
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
Cleared hypotheses: hy
-- 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 : 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⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
have 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⁆
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
Cleared hypotheses: hy
-- 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 : 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⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
have 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⁆
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
Cleared hypotheses: hy
-- 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 : 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⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
have mem₃ : ∀ (v : L) (hv : Membership.mem (γ := Set L) {e, f, h} v), Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, v⁆
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
Cleared hypotheses: hy
-- 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 : 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
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅x, y⁆
have zero : Membership.mem (γ := Submodule R L) (span R {e, f, h}) (Bracket.bracket (L := L) 0 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
Cleared hypotheses: hx
-- 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 : 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)
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅x, y⁆
have 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⁆
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
Cleared hypotheses: hx
-- 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 : 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⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅x, y⁆
have 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⁆
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
Cleared hypotheses: hx