awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
rw : Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) ⊥
rw₁ : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
⊢ Function.Injective (α := L) (β := LieDerivation R L L) (⇑(ad R L) : (a : L) → LieDerivation R L L)
have rw₂ : Eq.{u_2 + 1} (α := LieIdeal R L) ⊥ ⊥
Tactic: rw [← LieHom.ker_eq_bot, ad_ker_eq_center, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
x : L
⊢ Eq (α := LieDerivation R L L) (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
have rw : ⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ = -⁅x, D⁆
Tactic: rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
x : L
rw : ⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ = -⁅x, D⁆
⊢ Eq (α := LieDerivation R L L) (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
have rw₁ : ⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ =
  -Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D
Tactic: rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
x : L
rw : ⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ = -⁅x, D⁆
rw₁ :
  ⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ =
    -Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D
⊢ Eq (α := LieDerivation R L L) (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
have rw₂ : Eq (α := LieDerivation R L L) (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
  (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
Tactic: rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ LieHom.IsIdealMorphism (L' := LieDerivation R L L) (ad R L)
have simp_rw : ∀ (x : LieDerivation R L L) (y : L),
  ∃ (z : L),
    Eq (α := LieDerivation R L L)
      ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
      ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)
Tactic: simp_rw [LieHom.isIdealMorphism_iff, lie_der_ad_eq_ad_der]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (x : LieDerivation R L L) (y : L),
    ∃ (z : L),
      Eq (α := LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)
⊢ ∀ (x : LieDerivation R L L) (y : L),
    ∃ (z : L),
      Eq (α := LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)
have h : ∀ (x : LieDerivation R L L) (y : L),
  Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (x : LieDerivation R L L) (y : L),
    ∃ (z : L),
      Eq (α := LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)
h :
  ∀ (x : LieDerivation R L L) (y : L),
    Eq (α := LieDerivation R L L)
      ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
      ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
⊢ ∀ (x : LieDerivation R L L) (y : L),
    ∃ (z : L),
      Eq (α := LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)
have w : LieDerivation R L L → L → L
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
⊢ Eq (α := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) ⊥
have refine : ∀ (D : LieDerivation R L L)
  (hD :
    Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L))
      D)
  (x : L), Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)
Tactic: refine (LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
D : LieDerivation R L L
hD :
  Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D
x : L
⊢ Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L) (0 : LieDerivation R L L)
have rw : ∀ (hD : ∀ (x : L), ⁅x, D⁆ = 0) (x : L),
  Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L) (0 : LieDerivation R L L)
Tactic: rw [LieModule.mem_maxTrivSubmodule] at hD
Cleared hypotheses: hD, x
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
D : LieDerivation R L L
hD :
  Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D
x : L
⊢ Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)
have this : Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
  (0 : LieDerivation R L L)
Tactic: have : ad R L (D x) = 0 := by
    rw [LieModule.mem_maxTrivSubmodule] at hD
    simp [ad_apply_lieDerivation, hD]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
D : LieDerivation R L L
hD :
  Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D
x : L
this :
  Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L) (0 : LieDerivation R L L)
⊢ Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)
have this₁ : Eq (α := L) ((D : (a : L) → L) x : L) (0 : L)
Tactic: rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.JordanChevalley (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
⊢ Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
have obtain : ∀ (n' : Module.End K (Module.End K V))
  (hn'_adj :
    Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
      K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
          Module.End K (Module.End K V))]
      n')
  (s' : Module.End K (Module.End K V))
  (hs'_adj :
    Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
      K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
          Module.End K (Module.End K V))]
      s')
  (hn'_nil : IsNilpotent n') (hs'_ss : s'.IsSemisimple)
  (h_jc : (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) = n' + s'),
  Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
Tactic: obtain ⟨n', hn'_adj, s', hs'_adj, hn'_nil, hs'_ss, h_jc⟩ :=
    (ad K _ (n + s)).exists_isNilpotent_isSemisimple
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.JordanChevalley (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj :
  Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    n'
s' : Module.End K (Module.End K V)
hs'_adj :
  Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    s'
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) = n' + s'
⊢ Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
have hc' : Commute n' s'
Tactic: have hc' : Commute n' s' :=
    Algebra.commute_of_mem_adjoin_singleton_of_commute hs'_adj
      (Algebra.commute_of_mem_adjoin_self hn'_adj).symm
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.JordanChevalley (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj :
  Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    n'
s' : Module.End K (Module.End K V)
hs'_adj :
  Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    s'
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
⊢ Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
have hs_eq : s' = (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s
Tactic: obtain ⟨-, hs_eq⟩ := Module.End.isNilpotent_isSemisimple_unique hn'_nil hs'_ss
    (LieAlgebra.ad_nilpotent_of_nilpotent (R := K) hn)
    (LieAlgebra.ad_isSemisimple_of_isSemisimple hs) hc'
    (LieAlgebra.commute_ad_of_commute hc) (h_jc.symm.trans (map_add (ad K _) n s))
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.JordanChevalley (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj :
  Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    n'
s' : Module.End K (Module.End K V)
hs'_adj :
  Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    s'
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
hs_eq : s' = (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s
⊢ Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
have rwa : ∀
  (hs'_adj :
    Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
      K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
          Module.End K (Module.End K V))]
      ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s :
        Module.End K (Module.End K V)))
  (hn'_nil : IsNilpotent n') (hs'_ss : s'.IsSemisimple)
  (h_jc : (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) = n' + s')
  (hc' : Commute n' s') (hs_eq : s' = (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s),
  Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
Tactic: rwa [hs_eq] at hs'_adj
Cleared hypotheses: hs'_adj, hn'_nil, hs'_ss, h_jc, hc', hs_eq
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.JordanChevalley (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
⊢ Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) n : Module.End K (Module.End K V))
have this : (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) n =
  HSub.hSub (α := Module.End K (Module.End K V)) (β := Module.End K (Module.End K V))
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
      Module.End K (Module.End K V))
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
Tactic: have : ad K _ n = ad K _ (n + s) - ad K _ s := by simp [map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.JordanChevalley (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
this :
  (ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) n =
    HSub.hSub (α := Module.End K (Module.End K V)) (β := Module.End K (Module.End K V))
      ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))
      ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V))
⊢ Membership.mem (α := Module.End K (Module.End K V)) (γ := Subalgebra K (Module.End K (Module.End K V)))
    K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
        Module.End K (Module.End K V))]
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) n : Module.End K (Module.End K V))
have rw : Membership.mem (γ := Subalgebra K (Module.End K (Module.End K V)))
  K[((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
      Module.End K (Module.End K V))]
  (HSub.hSub (α := Module.End K (Module.End K V)) (β := Module.End K (Module.End K V))
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) (n + s) :
      Module.End K (Module.End K V))
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) s : Module.End K (Module.End K V)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x : A ⊗[R] L
⊢ Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        x :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
have refine_1 : Eq (α := A ⊗[R] L) (((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) 0 : (a : A ⊗[R] L) → A ⊗[R] L) 0) 0
Tactic: refine x.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x : A ⊗[R] L
refine_1 :
  Eq (α := A ⊗[R] L) (((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) 0 : (a : A ⊗[R] L) → A ⊗[R] L) 0) 0
⊢ Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        x :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
have refine_2 : ∀ (x : A) (y : L),
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x ⊗ₜ[R] y) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        (x ⊗ₜ[R] y) :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
Tactic: refine x.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x : A ⊗[R] L
refine_1 :
  Eq (α := A ⊗[R] L) (((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) 0 : (a : A ⊗[R] L) → A ⊗[R] L) 0) 0
refine_2 :
  ∀ (x : A) (y : L),
    Eq (α := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x ⊗ₜ[R] y) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (x ⊗ₜ[R] y) :
        A ⊗[R] L)
      (0 : A ⊗[R] L)
⊢ Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        x :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
have refine_3 : ∀ (x y : A ⊗[R] L),
  Eq (α := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          x :
        A ⊗[R] L)
      (0 : A ⊗[R] L) →
    Eq (α := A ⊗[R] L)
        ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            y :
          A ⊗[R] L)
        (0 : A ⊗[R] L) →
      Eq (α := A ⊗[R] L)
        ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x + y) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            (x + y) :
          A ⊗[R] L)
        (0 : A ⊗[R] L)
Tactic: refine x.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₁ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₁ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
h₂ :
  Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₂ :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
this :
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₁ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          z₂ :
        A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) z₂ : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          z₁ :
        A ⊗[R] L) =
    0
⊢ Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (z₁ + z₂) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        (z₁ + z₂) :
      A ⊗[R] L)
    (0 : A ⊗[R] L)
have rw : HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (z₁ + z₂) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₁ :
      A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (z₁ + z₂) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        z₂ :
      A ⊗[R] L) =
  0
Tactic: rw [map_add, map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
        zero_add, add_zero, add_comm, this]