awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x_1 : A
l : L
x_2 x_3 : A ⊗[R] L
h1 :
  (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) x_2) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
        A ⊗[R] L)
      (⁅x_2, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)⁆ : A ⊗[R] L)
h2 :
  (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) x_3) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_3) :
        A ⊗[R] L)
      (⁅x_3, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)⁆ : A ⊗[R] L)
⊢ (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l) (x_2 + x_3)) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] l)
          ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_2 + x_3)) :
        A ⊗[R] L)
      (⁅x_2 + x_3, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] l)⁆ : A ⊗[R] L)

Tactic:
simp [h1, h2, sub_add_sub_comm]

Premises used: sub_add_sub_comm
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x y x_1 x_2 : A ⊗[R] L
h1 :
  (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x_1, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x_1, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_1⁆ : A ⊗[R] L)
h2 :
  (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x_2, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x_2, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2⁆ : A ⊗[R] L)
⊢ (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x_1 + x_2, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x_1 + x_2, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 + x_2)⁆ : A ⊗[R] L)

Tactic:
simp [h1, h2, sub_add_sub_comm]

Premises used: sub_add_sub_comm
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x x_1 : Derivation R A A
H :
  ∀ (a : A ⊗[R] L),
    Eq (α := A ⊗[R] L)
      (({ toFun := (⇑(LinearMap.rTensor L (↑(x + x_1) : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          a :
        A ⊗[R] L)
      ((HAdd.hAdd (α := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
              { toFun := (⇑(LinearMap.rTensor L (↑x : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯, leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }
              { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯, leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          a :
        A ⊗[R] L)
⊢ { toFun := (⇑(LinearMap.rTensor L (↑(x + x_1) : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
      map_smul' := ⋯, leibniz' := ⋯ } =
    HAdd.hAdd (α := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
      { toFun := (⇑(LinearMap.rTensor L (↑x : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }
      { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x x_1 : Derivation R A A
a : A ⊗[R] L
⊢ Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.rTensor L (↑(x + x_1) : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
            map_smul' := ⋯, leibniz' := ⋯ } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)
    ((HAdd.hAdd (α := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
            { toFun := (⇑(LinearMap.rTensor L (↑x : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }
            { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x : R
x_1 : Derivation R A A
H :
  ∀ (a : A ⊗[R] L),
    Eq (α := A ⊗[R] L)
      (({ toFun := (⇑(LinearMap.rTensor L (↑(x • x_1) : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          a :
        A ⊗[R] L)
      ((HSMul.hSMul (α := R) (β := LieDerivation R (A ⊗[R] L) (A ⊗[R] L)) ((RingHom.id R : (a : R) → R) x : R)
              { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯, leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          a :
        A ⊗[R] L)
⊢ { toFun := (⇑(LinearMap.rTensor L (↑(x • x_1) : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
      map_smul' := ⋯, leibniz' := ⋯ } =
    HSMul.hSMul (α := R) (β := LieDerivation R (A ⊗[R] L) (A ⊗[R] L)) ((RingHom.id R : (a : R) → R) x : R)
      { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) }

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x : R
x_1 : Derivation R A A
a : A ⊗[R] L
⊢ Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.rTensor L (↑(x • x_1) : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
            map_smul' := ⋯, leibniz' := ⋯ } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)
    ((HSMul.hSMul (α := R) (β := LieDerivation R (A ⊗[R] L) (A ⊗[R] L)) ((RingHom.id R : (a : R) → R) x : R)
            { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ : LieDerivation R (A ⊗[R] L) (A ⊗[R] L) } :
          (a : A ⊗[R] L) → A ⊗[R] L)
        a :
      A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x x_1 : Derivation R A A
H :
  ∀ (z : A ⊗[R] L),
    Eq (α := A ⊗[R] L)
      (({ toFun := (⇑(LinearMap.rTensor L (↑⁅x, x_1⁆ : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          z :
        A ⊗[R] L)
      ((Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
              { toFun := (⇑(LinearMap.rTensor L (↑x : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯, leibniz' := ⋯ }
              { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯, leibniz' := ⋯ } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          z :
        A ⊗[R] L)
⊢ Eq (α := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
    { toFun := (⇑(LinearMap.rTensor L (↑⁅x, x_1⁆ : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
      map_smul' := ⋯, leibniz' := ⋯ }
    (Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
      { toFun := (⇑(LinearMap.rTensor L (↑x : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ }
      { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯,
        leibniz' := ⋯ })

Tactic:
ext z
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x x_1 : Derivation R A A
z : A ⊗[R] L
⊢ Eq (α := A ⊗[R] L)
    (({ toFun := (⇑(LinearMap.rTensor L (↑⁅x, x_1⁆ : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
          map_smul' := ⋯, leibniz' := ⋯ } :
        (a : A ⊗[R] L) → A ⊗[R] L)
      0)
    ((Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
          { toFun := (⇑(LinearMap.rTensor L (↑x : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
            map_smul' := ⋯, leibniz' := ⋯ }
          { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
            map_smul' := ⋯, leibniz' := ⋯ } :
        (a : A ⊗[R] L) → A ⊗[R] L)
      0)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x x_1 : Derivation R A A
z : A ⊗[R] L
⊢ ∀ (x_2 : A) (y : L),
    Eq (α := A ⊗[R] L)
      (({ toFun := (⇑(LinearMap.rTensor L (↑⁅x, x_1⁆ : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
              map_smul' := ⋯, leibniz' := ⋯ } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (x_2 ⊗ₜ[R] y) :
        A ⊗[R] L)
      ((Bracket.bracket (L := LieDerivation R (A ⊗[R] L) (A ⊗[R] L))
              { toFun := (⇑(LinearMap.rTensor L (↑x : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯, leibniz' := ⋯ }
              { toFun := (⇑(LinearMap.rTensor L (↑x_1 : A →ₗ[R] A)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯, leibniz' := ⋯ } :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (x_2 ⊗ₜ[R] y) :
        A ⊗[R] L)

Tactic:
simp [sub_tmul]

Premises used: TensorProduct.sub_tmul
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x x_1 : Derivation R A A
z x_2 x_3 : A ⊗[R] L
hx :
  (LinearMap.rTensor L ⁅(↑x : A →ₗ[R] A), (↑x_1 : A →ₗ[R] A)⁆ : (a : A ⊗[R] L) → A ⊗[R] L) x_2 =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
          ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
        A ⊗[R] L)
      ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
          ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
        A ⊗[R] L)
hy :
  (LinearMap.rTensor L ⁅(↑x : A →ₗ[R] A), (↑x_1 : A →ₗ[R] A)⁆ : (a : A ⊗[R] L) → A ⊗[R] L) x_3 =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
          ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_3) :
        A ⊗[R] L)
      ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
          ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_3) :
        A ⊗[R] L)
⊢ HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
          A ⊗[R] L)
        ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
          A ⊗[R] L) +
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_3) :
          A ⊗[R] L)
        ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_3) :
          A ⊗[R] L) =
    HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
        ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
          A ⊗[R] L)
        ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_3) :
          A ⊗[R] L) -
      HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
        ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_2) :
          A ⊗[R] L)
        ((LinearMap.rTensor L (↑x_1 : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L)
            ((LinearMap.rTensor L (↑x : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x_3) :
          A ⊗[R] L)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : Derivation R A A
x : A ⊗[R] L
⊢ Eq (α := A ⊗[R] L)
    ((((ofDerivation L : (a : Derivation R A A) → LieDerivation R (A ⊗[R] L) (A ⊗[R] L)) d :
            LieDerivation R (A ⊗[R] L) (A ⊗[R] L)) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        x :
      A ⊗[R] L)
    ((LinearMap.rTensor L (↑d : A →ₗ[R] A) : (a : A ⊗[R] L) → A ⊗[R] L) x : A ⊗[R] L)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : LieDerivation R L L
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x + y) =
      HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
        ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x : A ⊗[R] L)
        ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y : A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : LieDerivation R L L
⊢ ∀ (m : R) (x : A ⊗[R] L),
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (m • x) =
      HSMul.hSMul (α := R) (β := A ⊗[R] L) ((RingHom.id R : (a : R) → R) m : R)
        ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x : A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
simp :
  (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x⁆ : A ⊗[R] L)
⊢ ({ toFun := (⇑(LinearMap.lTensor A (↑d : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯, map_smul' := ⋯ } :
        (a : A ⊗[R] L) → A ⊗[R] L)
      ⁅x, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x,
          ({ toFun := (⇑(LinearMap.lTensor A (↑d : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯ : A ⊗[R] L →ₗ[R] A ⊗[R] L } :
              (a : A ⊗[R] L) → A ⊗[R] L)
            y⁆ :
        A ⊗[R] L)
      (⁅y,
          ({ toFun := (⇑(LinearMap.lTensor A (↑d : L →ₗ[R] L)) : (a : A ⊗[R] L) → A ⊗[R] L), map_add' := ⋯,
                map_smul' := ⋯ : A ⊗[R] L →ₗ[R] A ⊗[R] L } :
              (a : A ⊗[R] L) → A ⊗[R] L)
            x⁆ :
        A ⊗[R] L)

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, AddHom.coe_mk
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (Bracket.bracket (L := A ⊗[R] L) 0 y) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) 0 ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
        A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) 0⁆ : A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
refine_1 :
  ∀ (x : A) (y_1 : L),
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x ⊗ₜ[R] y_1) y) =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x ⊗ₜ[R] y_1)
            ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
          A ⊗[R] L)
        (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)
refine_2 :
  ∀ (x y_1 : A ⊗[R] L),
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x, y⁆ =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (⁅x, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
          (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x⁆ : A ⊗[R] L) →
      (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅y_1, y⁆ =
          HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
            (⁅y_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
            (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y_1⁆ : A ⊗[R] L) →
        (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x + y_1, y⁆ =
          HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
            (⁅x + y_1, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
            (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x + y_1)⁆ : A ⊗[R] L)
⊢ (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) ⁅x, y⁆ =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (⁅x, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y⁆ : A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x⁆ : A ⊗[R] L)

Tactic:
refine x.induction_on (by simp) ?_ ?_
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x_1 : A
y_1 : L
⊢ (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) 0) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) 0) :
        A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) 0
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)) :
        A ⊗[R] L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.BaseChange
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x_1 : A
y_1 : L
refine_1 :
  ∀ (x : A) (y : L),
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) (x ⊗ₜ[R] y)) =
      HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
            ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x ⊗ₜ[R] y)) :
          A ⊗[R] L)
        (Bracket.bracket (L := A ⊗[R] L) (x ⊗ₜ[R] y)
            ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)) :
          A ⊗[R] L)
refine_1₁ :
  ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) x) =
        HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
          (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
              ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) x) :
            A ⊗[R] L)
          (⁅x, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L) →
      (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
            (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) y) =
          HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
            (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
                ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
              A ⊗[R] L)
            (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L) →
        (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
            (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) (x + y)) =
          HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
            (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
                ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x + y)) :
              A ⊗[R] L)
            (⁅x + y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)
⊢ (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1) y) =
    HSub.hSub (α := A ⊗[R] L) (β := A ⊗[R] L)
      (Bracket.bracket (L := A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)
          ((LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) y) :
        A ⊗[R] L)
      (⁅y, (LinearMap.lTensor A (↑d : L →ₗ[R] L) : (a : A ⊗[R] L) → A ⊗[R] L) (x_1 ⊗ₜ[R] y_1)⁆ : A ⊗[R] L)

Tactic:
refine y.induction_on (by simp) ?_ ?_