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
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 : ι
⊢ b.symm.baseSupp i = (-b.baseSupp) i
have 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)
Tactic: change ∑ j, b.A i j • b₂.coord j = - ∑ j, b.A i j • b₁.coord j
-- 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
⊢ b.symm.baseSupp = -b.baseSupp
have suffices : b₁.coord = -b₂.coord
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]
-- 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
⊢ b₁.coord = -b₂.coord
have simp : ((Basis.span sorry).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) sorry).symm).coord =
  -(Basis.map
        ((Basis.span sorry).map
          (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (Submodule.span R (range b.h)) (Submodule.span R (range (-b.h))) sorry))
        (LinearEquiv.ofEq b.symm.cartan.toSubmodule (Submodule.span R (range b.symm.h)) sorry).symm).coord
Tactic: simp only [b₁, b₂, Basis.span_neg b.linInd]
-- 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 ι
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)
have rw : Ne (α := R) (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) b.A.det : R) (0 : R)
Tactic: rw [Matrix.nondegenerate_iff_det_ne_zero, ← RingHom.map_det]
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
⊢ 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)
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
-- 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 ι
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 b.baseSupp
have hv : LinearIndependent R v
Tactic: have hv : LinearIndependent R v := Basis.linearIndependent_coord _
-- 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 ι
inst_5 : IsDomain R
inst_6 : CharZero R
⊢ LinearIndependent R b.baseSupp
have have : Matrix.Nondegenerate.{u_1, u_1, u_2} (m := ι) (n := ι) (R := R)
  ((RingHom.mapMatrix (Int.castRingHom R) : (a : Matrix ι ι ℤ) → Matrix ι ι R) b.A)
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
-- 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 ι
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)
⊢ LinearIndependent R b.baseSupp
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
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
-- 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 ι
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
⊢ LinearIndependent R b.baseSupp
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)),
  let v := ((Basis.span sorry).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (range b.h)) sorry).symm).coord;
  ∀ (hv : LinearIndependent R v), 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
-- 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 : ι
x : ↥b.cartan
⊢ 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⁆
have 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⁆
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- 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 : ι
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⁆
have 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⁆
Tactic: simp only [coe_bracket_of_module]
-- 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 : ι
x : L
hx : x ∈ b.cartan
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
have rwa : ∀ (hx : x ∈ b.cartan.toSubmodule), Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
Tactic: rwa [← LieSubalgebra.mem_toSubmodule, coe_cartan_eq_span] at hx
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 : ι
x : L
hx : x ∈ b.cartan
rwa : ∀ (hx : x ∈ b.cartan.toSubmodule), Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
have 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
Tactic: rwa [← LieSubalgebra.mem_toSubmodule, coe_cartan_eq_span] at hx
Cleared hypotheses: hx
-- 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 : ι
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) =
    ⁅x, b.e i⁆
have hx' : 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
-- 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 : ι
x 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⁆
have 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⁆
Tactic: obtain ⟨j, rfl⟩ := hu
Cleared hypotheses: u, hu, 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 : ι
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) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (b.h j) hx) : R) (b.e i) =
    ⁅b.h j, b.e i⁆
have 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⁆
Tactic: change b.baseSupp i (b.h' j) • _ = _
-- 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 : ι
x : L
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)
have 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)
Tactic: change b.baseSupp i 0 • _ = _
-- 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 : ι
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
⊢ 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⁆
have 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⁆
Tactic: rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
Cleared hypotheses: hu, hv, hu', hv', 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 : ι
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
⊢ 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⁆
have 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⁆
Tactic: rw [← AddMemClass.mk_add_mk _ u v hu hv]
-- 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 : ι
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
⊢ 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⁆
have 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⁆
Tactic: simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
-- 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 : ι
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
⊢ 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⁆
have 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⁆
Tactic: rw [hu', hv']
-- 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 : ι
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⁆
⊢ 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⁆
have add₁ : ⁅u, b.e i⁆ + ⁅v, b.e i⁆ = ⁅u, b.e i⁆ + ⁅v, b.e i⁆
Tactic: rw [hu', hv']
-- 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 : ι
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
⊢ 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⁆
have 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⁆
Tactic: rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
Cleared hypotheses: hu, hv', 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 : ι
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
⊢ 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⁆
have 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⁆
Tactic: rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
-- 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 : ι
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⁆
⊢ 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⁆
have 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⁆
Tactic: rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]