-- 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
⊢ 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)
    (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
Tactic: rw [map_add, map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
        zero_add, add_zero, add_comm, this]