awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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
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))
⊢ 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

Premises used: Module.End.exists_isNilpotent_isSemisimple
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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'
⊢ 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
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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'
⊢ 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))

Premises used: LieAlgebra.ad_isSemisimple_of_isSemisimple, LieAlgebra.ad, map_add, LieAlgebra.ad_nilpotent_of_nilpotent, Module.End.isNilpotent_isSemisimple_unique, LieAlgebra.commute_ad_of_commute, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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
rwa rwa₁ rwa₂ 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))
⊢ 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
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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
⊢ (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:
simp [map_add]

Premises used: map_add
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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
⊢ (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]
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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))
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)))
⊢ 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))

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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 (γ := 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:
sub_mem (Algebra.self_mem_adjoin_singleton K _) (ad_mem_adjoin_of_isSemisimple hc hn hs)

Premises used: Set.Mem, sub_mem, LieAlgebra.ad_mem_adjoin_of_isSemisimple, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
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 (γ := 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:
exact sub_mem (Algebra.self_mem_adjoin_singleton K _) (ad_mem_adjoin_of_isSemisimple hc hn hs)

Premises used: sub_mem, LieAlgebra.ad_mem_adjoin_of_isSemisimple, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
s t : A
x : L
m : M
⊢ Eq (α := A ⊗[R] M)
    ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (s ⊗ₜ[R] x) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        (t ⊗ₜ[R] m) :
      A ⊗[R] M)
    ((s * t) ⊗ₜ[R] ⁅x, m⁆ : A ⊗[R] M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
x : A ⊗[R] L
m : A ⊗[R] M
⊢ ⁅x, m⁆ =
    (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) x : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
s t : A
x : L
y : M
⊢ Eq (α := A ⊗[R] M) (Bracket.bracket (L := A ⊗[R] L) (s ⊗ₜ[R] x) (t ⊗ₜ[R] y)) ((s * t) ⊗ₜ[R] ⁅x, y⁆)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Lie.BaseChange
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)

Tactic:
x.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Lie.BaseChange
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)
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)
⊢ 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)

Tactic:
refine x.induction_on ?_ ?_ ?_
-- Module: Mathlib.Algebra.Lie.BaseChange
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) 0 : (a : A ⊗[R] L) → A ⊗[R] L) 0) 0

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.Lie.BaseChange
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
a : A
l : L
⊢ Eq (α := A ⊗[R] L)
    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a ⊗ₜ[R] l) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        (a ⊗ₜ[R] l) :
      A ⊗[R] L)
    (0 : A ⊗[R] L)

Tactic:
simp only [bracket'_tmul, TensorProduct.tmul_zero, lie_self]

Premises used: _private.0.LieAlgebra.ExtendScalars.bracket'_tmul, TensorProduct.tmul_zero, lie_self
-- Module: Mathlib.Algebra.Lie.BaseChange
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)
refine_3 :
  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)

Tactic:
suffices bracket' R A L L z₁ z₂ + bracket' R A L L z₂ z₁ = 0 by
      rw [map_add, map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
        zero_add, add_zero, add_comm, this]
-- Module: Mathlib.Algebra.Lie.BaseChange
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)
⊢ 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

Tactic:
z₁.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Lie.BaseChange
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)
⊢ HAdd.hAdd (α := A ⊗[R] L) (β := 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) 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)
          0 :
        A ⊗[R] L) =
    0

Tactic:
simp only [map_zero, add_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero, add_zero
-- Module: Mathlib.Algebra.Lie.BaseChange
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)
a₁ : A
l₁ : L
⊢ HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) : 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)
          (a₁ ⊗ₜ[R] l₁) :
        A ⊗[R] L) =
    0

Tactic:
z₂.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Lie.BaseChange
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)
a₁ : A
l₁ : L
⊢ HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          0 :
        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) (a₁ ⊗ₜ[R] l₁) :
        A ⊗[R] L) =
    0

Tactic:
simp only [map_zero, add_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero, add_zero