awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅zc, yl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: rw [← lie_skew, neg_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅zc, yu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: rw [← lie_skew, neg_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yl, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅zu, yl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: rw [← lie_skew, neg_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) x
⊢ x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have mem : ∀ (u : L) (hu : u ∈ range b.e ∪ range b.f), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ b.cartan) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using hu
    obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ b.cartan) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using hv
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) x
mem : ∀ (u : L) (hu : u ∈ range b.e ∪ range b.f), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have zero : 0 ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ b.cartan) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using hu
    obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ b.cartan) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using hv
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) x
mem : ∀ (u : L) (hu : u ∈ range b.e ∪ range b.f), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zero : 0 ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have add : ∀ (u v : L),
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u →
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v →
      ∀ (hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper)
        (hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper),
        u + v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ b.cartan) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using hu
    obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ b.cartan) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using hv
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) x
mem : ∀ (u : L) (hu : u ∈ range b.e ∪ range b.f), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zero : 0 ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
add :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v →
        ∀ (hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper)
          (hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper),
          u + v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have smul : ∀ (t : R) (u : L),
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u →
    ∀ (hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper),
      t • u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ b.cartan) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using hu
    obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ b.cartan) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using hv
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
⊢ Eq.{u_2 + 1} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) ((↑(b.A i j) : R) : R)
have simp : Eq.{u_2 + 1} (α := R)
  (∑ c : ι,
    (b.A i c •
          ((Basis.span sorry).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) sorry).symm).coord c :
        (a : ↥b.cartan) → R)
      (b.h' j))
  (↑(b.A i j) : R)
Tactic: simp only [baseSupp, LinearMap.coe_sum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
e : ↥b.cartan.toSubmodule ≃ₗ[R] ↥(Submodule.span R (range b.h)) :=
  LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯
f : (k : ι) → R :=
  fun (k : ι) ↦
    HSMul.hSMul (β := R) (b.A i k)
      (((((Basis.span ⋯).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
                ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
              ι →₀ R) :
            (a : ι) → R)
          k :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ c : ι,
      (b.A i c •
            ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord c :
          (a : ↥b.cartan) → R)
        (b.h' j))
    (↑(b.A i j) : R)
have change : Eq.{u_2 + 1} (α := R) (∑ k : ι, f k) (↑(b.A i j) : R)
Tactic: change ∑ k, f k = _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
e : ↥b.cartan.toSubmodule ≃ₗ[R] ↥(Submodule.span R (range b.h)) :=
  LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯
f : (k : ι) → R :=
  fun (k : ι) ↦
    HSMul.hSMul (β := R) (b.A i k)
      (((((Basis.span ⋯).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
                ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
              ι →₀ R) :
            (a : ι) → R)
          k :
        R)
⊢ f = fun (k : ι) ↦ if j = k then (↑(b.A i k) : R) else 0
have this : Eq (α := ι →₀ R)
  (((Basis.span sorry).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
      ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
    ι →₀ R)
  (Finsupp.single j 1 : ι →₀ R)
Tactic: have : (Basis.span b.linInd).repr (e <| b.h' j) = .single j 1 := Basis.span_repr_eq_single _ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
e : ↥b.cartan.toSubmodule ≃ₗ[R] ↥(Submodule.span R (range b.h)) :=
  LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯
f : (k : ι) → R :=
  fun (k : ι) ↦
    HSMul.hSMul (β := R) (b.A i k)
      (((((Basis.span ⋯).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
                ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
              ι →₀ R) :
            (a : ι) → R)
          k :
        R)
this :
  Eq (α := ι →₀ R)
    (((Basis.span ⋯).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
        ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
      ι →₀ R)
    (Finsupp.single j 1 : ι →₀ R)
⊢ f = fun (k : ι) ↦ if j = k then (↑(b.A i k) : R) else 0
have h : ∀ (k : ι), f k = if j = k then (↑(b.A i k) : R) else 0
Tactic: ext k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
e : ↥b.cartan.toSubmodule ≃ₗ[R] ↥(Submodule.span R (range b.h)) :=
  LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯
f : (k : ι) → R :=
  fun (k : ι) ↦
    HSMul.hSMul (β := R) (b.A i k)
      (((((Basis.span ⋯).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
                ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
              ι →₀ R) :
            (a : ι) → R)
          k :
        R)
⊢ Eq.{u_2 + 1} (α := R) (∑ k : ι, f k) (↑(b.A i j) : R)
have this : f = fun (k : ι) ↦ if j = k then (↑(b.A i k) : R) else 0
Tactic: have : f = fun k ↦ if j = k then (b.A i k : R) else 0 := by
    have : (Basis.span b.linInd).repr (e <| b.h' j) = .single j 1 := Basis.span_repr_eq_single _ _
    ext k
    simp [f, this, Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
⊢ Eq.{u_2 + 1} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) ((↑(b.A i j) : R) : R)
have simp : Eq.{u_2 + 1} (α := R)
  (∑ c : ι,
    (b.A i c •
          ((Basis.span sorry).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) sorry).symm).coord c :
        (a : ↥b.cartan) → R)
      (b.h' j))
  (↑(b.A i j) : R)
Tactic: classical
  simp only [baseSupp, LinearMap.coe_sum, Finset.sum_apply]
  let e := LinearEquiv.ofEq _ _ b.coe_cartan_eq_span
  let f (k : ι) : R := b.A i k • (Basis.span b.linInd).repr (e <| b.h' j) k
  change ∑ k, f k = _
  have : f = fun k ↦ if j = k then (b.A i k : R) else 0 := by
    have : (Basis.span b.linInd).repr (e <| b.h' j) = .single j 1 := Basis.span_repr_eq_single _ _
    ext k
    simp [f, this, Finsupp.single_apply]
  simp [this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
simp :
  Eq.{u_2 + 1} (α := R)
    (∑ c : ι,
      (b.A i c •
            ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord c :
          (a : ↥b.cartan) → R)
        (b.h' j))
    (↑(b.A i j) : R)
simp₁ simp₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ c : ι,
      (b.A i c •
            ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord c :
          (a : ↥b.cartan) → R)
        (b.h' j))
    (↑(b.A i j) : R)
⊢ Eq.{u_2 + 1} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) ((↑(b.A i j) : R) : R)
have simp₃ : let e := LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) sorry;
let f : (k : ι) → R := fun (k : ι) ↦
  HSMul.hSMul (β := R) (b.A i k)
    (((((Basis.span sorry).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
              ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
            ι →₀ R) :
          (a : ι) → R)
        k :
      R);
Eq.{u_2 + 1} (α := R) (∑ k : ι, f k) (↑(b.A i j) : R)
Tactic: classical
  simp only [baseSupp, LinearMap.coe_sum, Finset.sum_apply]
  let e := LinearEquiv.ofEq _ _ b.coe_cartan_eq_span
  let f (k : ι) : R := b.A i k • (Basis.span b.linInd).repr (e <| b.h' j) k
  change ∑ k, f k = _
  have : f = fun k ↦ if j = k then (b.A i k : R) else 0 := by
    have : (Basis.span b.linInd).repr (e <| b.h' j) = .single j 1 := Basis.span_repr_eq_single _ _
    ext k
    simp [f, this, Finsupp.single_apply]
  simp [this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
i j : ι
simp :
  Eq.{u_2 + 1} (α := R)
    (∑ c : ι,
      (b.A i c •
            ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord c :
          (a : ↥b.cartan) → R)
        (b.h' j))
    (↑(b.A i j) : R)
simp₁ simp₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ c : ι,
      (b.A i c •
            ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord c :
          (a : ↥b.cartan) → R)
        (b.h' j))
    (↑(b.A i j) : R)
simp₃ :
  let e := LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯;
  let f : (k : ι) → R := fun (k : ι) ↦
    HSMul.hSMul (β := R) (b.A i k)
      (((((Basis.span ⋯).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
                ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
              ι →₀ R) :
            (a : ι) → R)
          k :
        R);
  Eq.{u_2 + 1} (α := R) (∑ k : ι, f k) (↑(b.A i j) : R)
⊢ Eq.{u_2 + 1} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) ((↑(b.A i j) : R) : R)
have simp₄ : let e := LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) sorry;
let f : (k : ι) → R := fun (k : ι) ↦
  HSMul.hSMul (β := R) (b.A i k)
    (((((Basis.span sorry).repr : (a : ↥(Submodule.span R (range b.h))) → ι →₀ R)
              ((e : (a : ↥b.cartan.toSubmodule) → ↥(Submodule.span R (range b.h))) (b.h' j)) :
            ι →₀ R) :
          (a : ι) → R)
        k :
      R);
∀ (this : f = fun (k : ι) ↦ if j = k then (↑(b.A i k) : R) else 0),
  Eq.{u_2 + 1} (α := R) (∑ k : ι, f k) (↑(b.A i j) : R)
Tactic: classical
  simp only [baseSupp, LinearMap.coe_sum, Finset.sum_apply]
  let e := LinearEquiv.ofEq _ _ b.coe_cartan_eq_span
  let f (k : ι) : R := b.A i k • (Basis.span b.linInd).repr (e <| b.h' j) k
  change ∑ k, f k = _
  have : f = fun k ↦ if j = k then (b.A i k : R) else 0 := by
    have : (Basis.span b.linInd).repr (e <| b.h' j) = .single j 1 := Basis.span_repr_eq_single _ _
    ext k
    simp [f, this, Finsupp.single_apply]
  simp [this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
b₁ : Module.Basis.{u_1, u_2, u_3} ι R ↥b.cartan :=
  (Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm
b₂ : Module.Basis.{u_1, u_2, u_3} ι R ↥b.cartan :=
  (Basis.span ⋯).map (LinearEquiv.ofEq b.symm.cartan.toSubmodule (Submodule.span R (range b.symm.h)) ⋯).symm
this : b₁.coord = -b₂.coord
⊢ b.symm.baseSupp = -b.baseSupp
have h : ∀ (i : ι), b.symm.baseSupp i = (-b.baseSupp) i
Tactic: ext1 i