awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basis
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, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl

Premises used: LieSubmodule.mem_sup_right, LieSubmodule.mem_sup_left, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Basis
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, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl

Premises used: LieSubmodule.mem_sup_right, LieSubmodule.mem_sup_left, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Basis
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, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl

Premises used: _private.0.LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top_aux
-- Module: Mathlib.Algebra.Lie.Basis
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, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl

Premises used: _private.0.LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top_aux
-- Module: Mathlib.Algebra.Lie.Basis
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
⊢ ⁅yc, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu

Premises used: LieSubmodule.mem_sup_right, LieSubmodule.lie_mem, LieAlgebra.Basis.borelUpper
-- Module: Mathlib.Algebra.Lie.Basis
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
⊢ ⁅yc, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu

Premises used: LieSubmodule.mem_sup_right, LieSubmodule.lie_mem, LieAlgebra.Basis.borelUpper
-- Module: Mathlib.Algebra.Lie.Basis
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
lie : ⁅zu, yl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yl, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
rw [← lie_skew, neg_mem_iff]

Premises used: neg_mem_iff, lie_skew
-- Module: Mathlib.Algebra.Lie.Basis
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
⊢ ⁅zu, yl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl

Premises used: _private.0.LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top_aux
-- Module: Mathlib.Algebra.Lie.Basis
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
⊢ ⁅zu, yl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl

Premises used: _private.0.LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top_aux
-- Module: Mathlib.Algebra.Lie.Basis
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, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu

Premises used: LieSubmodule.mem_sup_right, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Basis
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, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu

Premises used: LieSubmodule.mem_sup_right, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Basis
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)
⊢ Eq.{u_2 + 1} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) ((↑(b.A i j) : R) : R)

Tactic:
simp only [baseSupp, LinearMap.coe_sum, Finset.sum_apply]

Premises used: LieAlgebra.Basis.baseSupp, Finset.sum_apply, LinearMap.coe_sum
-- Module: Mathlib.Algebra.Lie.Basis
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)
change : Eq.{u_2 + 1} (α := R) (∑ k : ι, f k) (↑(b.A i j) : 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)

Tactic:
change ∑ k, f k = _
-- Module: Mathlib.Algebra.Lie.Basis
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 (α := ι →₀ 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)

Tactic:
have : (Basis.span b.linInd).repr (e <| b.h' j) = .single j 1 := Basis.span_repr_eq_single _ _
-- Module: Mathlib.Algebra.Lie.Basis
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)
h : ∀ (k : ι), f k = if j = k then (↑(b.A i k) : R) else 0
⊢ f = fun (k : ι) ↦ if j = k then (↑(b.A i k) : R) else 0

Tactic:
ext k
-- Module: Mathlib.Algebra.Lie.Basis
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)
k : ι
⊢ f k = if j = k then (↑(b.A i k) : R) else 0

Tactic:
simp [f, this, Finsupp.single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Algebra.Lie.Basis
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

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]
-- Module: Mathlib.Algebra.Lie.Basis
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 : 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:
simp [this]
-- Module: Mathlib.Algebra.Lie.Basis
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)
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);
  ∀ (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)
⊢ Eq.{u_2 + 1} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) ((↑(b.A i j) : R) : 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]

Premises used: LieAlgebra.Basis.baseSupp, Finset.sum_apply, LinearMap.coe_sum
-- Module: Mathlib.Algebra.Lie.Basis
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
h : ∀ (i : ι), b.symm.baseSupp i = (-b.baseSupp) i
⊢ b.symm.baseSupp = -b.baseSupp

Tactic:
ext1 i
-- Module: Mathlib.Algebra.Lie.Basis
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
i : ι
h :
  Eq (α := LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥b.cartan) R) (∑ j : ι, b.A i j • b₂.coord j)
    (-∑ j : ι, b.A i j • b₁.coord j)
⊢ b.symm.baseSupp i = (-b.baseSupp) i

Tactic:
change ∑ j, b.A i j • b₂.coord j = - ∑ j, b.A i j • b₁.coord j
-- Module: Mathlib.Algebra.Lie.Basis
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
i : ι
⊢ Eq (α := LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥b.cartan) R) (∑ j : ι, b.A i j • b₂.coord j)
    (-∑ j : ι, b.A i j • b₁.coord j)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Lie.Basis
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
suffices : b₁.coord = -b₂.coord
⊢ b.symm.baseSupp = -b.baseSupp

Tactic:
suffices b₁.coord = -b₂.coord by
    ext1 i
    change ∑ j, b.A i j • b₂.coord j = - ∑ j, b.A i j • b₁.coord j
    simp [this]