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
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
simp :
  ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord =
    -(Basis.map
          ((Basis.span ⋯).map
            (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (Submodule.span R (range b.h)) (Submodule.span R (range (-b.h))) ⋯))
          (LinearEquiv.ofEq b.symm.cartan.toSubmodule (Submodule.span R (range b.symm.h)) ⋯).symm).coord
⊢ b₁.coord = -b₂.coord

Tactic:
simp only [b₁, b₂, Basis.span_neg b.linInd]

Premises used: Module.Basis.span_neg, LieAlgebra.Basis.linInd
-- 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
⊢ ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord =
    -(Basis.map
          ((Basis.span ⋯).map
            (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (Submodule.span R (range b.h)) (Submodule.span R (range (-b.h))) ⋯))
          (LinearEquiv.ofEq b.symm.cartan.toSubmodule (Submodule.span R (range b.symm.h)) ⋯).symm).coord

Tactic:
aesop
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
rw : Ne (α := R) (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) b.A.det : R) (0 : R)
⊢ Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
    ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)

Tactic:
rw [Matrix.nondegenerate_iff_det_ne_zero, ← RingHom.map_det]

Premises used: RingHom.map_det, Matrix.nondegenerate_iff_det_ne_zero
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
⊢ Ne (α := R) (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) b.A.det : R) (0 : R)

Tactic:
simpa using b.nondegen.det_ne_zero

Premises used: LieAlgebra.Basis.nondegen, Matrix.Nondegenerate.det_ne_zero
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
⊢ Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
    ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)

Tactic:
have : ((Int.castRingHom R).mapMatrix b.A).Nondegenerate := by
    rw [Matrix.nondegenerate_iff_det_ne_zero, ← RingHom.map_det]
    simpa using b.nondegen.det_ne_zero
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
this :
  Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
    ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)
v : ι → Dual.{u_2, u_3} R ↥b.cartan :=
  ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord
⊢ LinearIndependent R v

Tactic:
have hv : LinearIndependent R v := Basis.linearIndependent_coord _
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
this :
  Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
    ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)
v : ι → Dual.{u_2, u_3} R ↥b.cartan :=
  ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord
hv : LinearIndependent R v
⊢ LinearIndependent R b.baseSupp

Tactic:
simpa [Int.cast_smul_eq_zsmul] using hv.sum_smul_of_nondegenerate this

Premises used: LinearIndependent.sum_smul_of_nondegenerate, Int.cast_smul_eq_zsmul
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
have :
  Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
    ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)
have₁ :
  ∀
    (this :
      Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
        ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)),
    LinearIndependent R b.baseSupp
have₂ :
  Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
    ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)
have₃ have₄ have₅ :
  ∀
    (this :
      Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
        ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)),
    LinearIndependent R b.baseSupp
have₆ :
  ∀
    (this :
      Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
        ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)),
    let v := ((Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord;
    ∀ (hv : LinearIndependent R v), LinearIndependent R b.baseSupp
⊢ LinearIndependent R b.baseSupp

Tactic:
classical
  have : ((Int.castRingHom R).mapMatrix b.A).Nondegenerate := by
    rw [Matrix.nondegenerate_iff_det_ne_zero, ← RingHom.map_det]
    simpa using b.nondegen.det_ne_zero
  let v : ι → Dual R b.cartan :=
    ((Basis.span b.linInd).map (LinearEquiv.ofEq _ _ b.coe_cartan_eq_span).symm).coord
  have hv : LinearIndependent R v := Basis.linearIndependent_coord _
  simpa [Int.cast_smul_eq_zsmul] using hv.sum_smul_of_nondegenerate this

Premises used: Int.cast_smul_eq_zsmul
-- 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 : ι
x : ↥b.cartan
obtain :
  ∀ (x : L) (hx : x ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
      ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) x : R) (b.e i) = ⁅x, b.e i⁆

Tactic:
obtain ⟨x, hx⟩ := x
-- 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 : ι
x : L
hx : x ∈ b.cartan
simp :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
    ⁅x, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
    ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx, b.e i⁆

Tactic:
simp only [coe_bracket_of_module]

Premises used: LieSubalgebra.coe_bracket_of_module
-- 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 : ι
x : L
hx : x ∈ b.cartan
rwa : ∀ (hx : x ∈ b.cartan.toSubmodule), Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x),
    Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x

Tactic:
rwa [← LieSubalgebra.mem_toSubmodule, coe_cartan_eq_span] at hx

Premises used: LieSubalgebra.mem_toSubmodule, LieAlgebra.Basis.coe_cartan_eq_span
-- 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 : ι
x : L
hx : x ∈ b.cartan
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x

Tactic:
have hx' : x ∈ Submodule.span R (range b.h) := by
    rwa [← LieSubalgebra.mem_toSubmodule, coe_cartan_eq_span] at hx
-- 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 : ι
x u : L
hu : u ∈ range b.h
hx : u ∈ b.cartan
mem :
  ∀ (j : ι) (hx : b.h j ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (b.h j) hx) : R) (b.e i) =
      ⁅b.h j, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
    ⁅u, b.e i⁆

Tactic:
obtain ⟨j, rfl⟩ := hu

Premises used: rfl
-- 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 : ι
x : L
j : ι
hx : b.h j ∈ b.cartan
mem : HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) (b.e i) = ⁅b.h j, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (b.h j) hx) : R) (b.e i) =
    ⁅b.h j, b.e i⁆

Tactic:
change b.baseSupp i (b.h' j) • _ = _

Premises used: LieAlgebra.Basis.baseSupp, LieAlgebra.Basis.h', DFunLike.coe
-- 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 : ι
x : L
j : ι
hx : b.h j ∈ b.cartan
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) (b.h' j) : R) (b.e i) = ⁅b.h j, b.e i⁆

Tactic:
simp [b.lie_h_e, Int.cast_smul_eq_zsmul]

Premises used: LieAlgebra.Basis.lie_h_e, Int.cast_smul_eq_zsmul
-- 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 : ι
x : L
hx : 0 ∈ b.cartan
zero :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) 0 : R) (b.e i) =
    Bracket.bracket (L := L) 0 (b.e i)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) 0 hx) : R) (b.e i) =
    Bracket.bracket (L := L) 0 (b.e i)

Tactic:
change b.baseSupp i 0 • _ = _

Premises used: LieAlgebra.Basis.baseSupp, OfNat.ofNat, DFunLike.coe
-- 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 : ι
x : L
hx : 0 ∈ b.cartan
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((b.baseSupp i : (a : ↥b.cartan) → R) 0 : R) (b.e i) =
    Bracket.bracket (L := L) 0 (b.e i)

Tactic:
simp
-- 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 : ι
x u v : L
hu : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) u
hv : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v
hu' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hv' :
  ∀ (hx : v ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
      ⁅v, b.e i⁆
hx : u + v ∈ b.cartan
add :
  ∀ (hu : u ∈ b.cartan) (hv : v ∈ b.cartan)
    (hu' :
      ∀ (hx : u ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
          ⁅u, b.e i⁆)
    (hv' :
      ∀ (hx : v ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
          ⁅v, b.e i⁆)
    (hx : u + v ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (u + v) hx) : R) (b.e i) =
      ⁅u + v, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (u + v) hx) : R) (b.e i) =
    ⁅u + v, b.e i⁆

Tactic:
rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv

Premises used: LieSubalgebra.mem_toSubmodule, LieAlgebra.Basis.coe_cartan_eq_span
-- 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 : ι
x u v : L
hu : u ∈ b.cartan
hv : v ∈ b.cartan
hu' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hv' :
  ∀ (hx : v ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
      ⁅v, b.e i⁆
hx : u + v ∈ b.cartan
add :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R)
          (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu + Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hv) :
        R)
      (b.e i) =
    ⁅u + v, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (u + v) hx) : R) (b.e i) =
    ⁅u + v, b.e i⁆

Tactic:
rw [← AddMemClass.mk_add_mk _ u v hu hv]

Premises used: AddMemClass.mk_add_mk
-- 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 : ι
x u v : L
hu : u ∈ b.cartan
hv : v ∈ b.cartan
hu' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hv' :
  ∀ (hx : v ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
      ⁅v, b.e i⁆
hx : u + v ∈ b.cartan
add :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hv) : R) (b.e i) =
    ⁅u, b.e i⁆ + ⁅v, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R)
          (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu + Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hv) :
        R)
      (b.e i) =
    ⁅u + v, b.e i⁆

Tactic:
simp only [map_add, add_smul, add_lie] at hu' hv' ⊢

Premises used: map_add, add_smul, add_lie
-- 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 : ι
x u v : L
hu : u ∈ b.cartan
hv : v ∈ b.cartan
hu' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hv' :
  ∀ (hx : v ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
      ⁅v, b.e i⁆
hx : u + v ∈ b.cartan
add :
  ⁅u, b.e i⁆ +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hv) : R) (b.e i) =
    ⁅u, b.e i⁆ + ⁅v, b.e i⁆
add₁ add₂ : ⁅u, b.e i⁆ + ⁅v, b.e i⁆ = ⁅u, b.e i⁆ + ⁅v, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hv) : R) (b.e i) =
    ⁅u, b.e i⁆ + ⁅v, b.e i⁆

Tactic:
rw [hu', hv']
-- 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 : ι
x : L
t : R
u : L
hu : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) u
hv' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hx : t • u ∈ b.cartan
smul :
  ∀ (hu : u ∈ b.cartan)
    (hv' :
      ∀ (hx : u ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
          ⁅u, b.e i⁆)
    (hx : t • u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
      ⁅t • u, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
    ⁅t • u, b.e i⁆

Tactic:
rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu

Premises used: LieSubalgebra.mem_toSubmodule, LieAlgebra.Basis.coe_cartan_eq_span
-- 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 : ι
x : L
t : R
u : L
hu : u ∈ b.cartan
hv' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hx : t • u ∈ b.cartan
smul :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (t • Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
    ⁅t • u, b.e i⁆
smul₁ :
  HSMul.hSMul (β := R) t
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) •
      b.e i =
    ⁅t • u, b.e i⁆
smul₂ :
  t •
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
    ⁅t • u, b.e i⁆
smul₃ : t • ⁅u, b.e i⁆ = ⁅t • u, b.e i⁆
smul₄ smul₅ : t • ⁅u, b.e i⁆ = t • ⁅u, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
    ⁅t • u, b.e i⁆

Tactic:
rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]

Premises used: smul_assoc, smul_lie, SetLike.mk_smul_mk, map_smul
-- 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 : ι
x : L
hx : x ∈ b.cartan
hx' : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
mem :
  ∀ (u : L) (hu : u ∈ range b.h) (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
zero :
  ∀ (hx : 0 ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) 0 hx) : R) (b.e i) =
      Bracket.bracket (L := L) 0 (b.e i)
add :
  ∀ (u v : L) (hu : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) u)
    (hv : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v)
    (hu' :
      ∀ (hx : u ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
          ⁅u, b.e i⁆)
    (hv' :
      ∀ (hx : v ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
          ⁅v, b.e i⁆)
    (hx : u + v ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (u + v) hx) : R) (b.e i) =
      ⁅u + v, b.e i⁆
smul :
  ∀ (t : R) (u : L) (hu : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) u)
    (hv' :
      ∀ (hx : u ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
          ⁅u, b.e i⁆)
    (hx : t • u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
      ⁅t • u, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
    ⁅x, b.e i⁆

Tactic:
induction hx' using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨j, rfl⟩ := hu
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]
  | zero => change b.baseSupp i 0 • _ = _; simp
  | add u v hu hv hu' hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
    rw [← AddMemClass.mk_add_mk _ u v hu hv]
    simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
    rw [hu', hv']
  | smul t u hu hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
    rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]

Premises used: LieAlgebra.Basis.baseSupp, smul_assoc, LieSubalgebra.mem_toSubmodule, LieAlgebra.Basis.coe_cartan_eq_span, map_add, smul_lie, add_smul, LieAlgebra.Basis.lie_h_e, OfNat.ofNat, DFunLike.coe, Int.cast_smul_eq_zsmul, rfl, map_smul, add_lie
-- 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 : ι
x : ↥b.cartan
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((b.symm.baseSupp i : (a : ↥b.symm.cartan) → R) x : R) (b.symm.e i) =
    ⁅x, b.symm.e i⁆

Tactic:
have := b.symm.baseSupp_apply_smul_e i x