-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.BaseChange (goal)
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 :
  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 :
      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 :
      A ⊗[R] L)
hy :
  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_3 :
      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_3 :
      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)
        (x_2 + x_3) :
      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 + x_3) :
      A ⊗[R] L)
have H : ∀
  (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: simp_all
Cleared hypotheses: hx, hy