-- 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
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
rw₁ :
  HAdd.hAdd (α := A ⊗[R] L) (β := A ⊗[R] L)
      ((HAdd.hAdd (α := A ⊗[R] L →ₗ[A] A ⊗[R] L) (β := A ⊗[R] L →ₗ[A] 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)
              ((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)
      ((HAdd.hAdd (α := A ⊗[R] L →ₗ[A] A ⊗[R] L) (β := A ⊗[R] L →ₗ[A] 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)
              ((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
rw₂ :
  HAdd.hAdd (β := 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))
      ((HAdd.hAdd (α := A ⊗[R] L →ₗ[A] A ⊗[R] L) (β := A ⊗[R] L →ₗ[A] 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)
              ((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
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₁ : 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) +
      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) (0 : 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) +
    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: rw [map_add, map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
        zero_add, add_zero, add_comm, this]