-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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 y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
refine_2 :
  (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        0) =
    HAdd.hAdd (α := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
              ((((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] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        0)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          0))
refine_2₁ :
  ∀ (x : A) (y : M),
    (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          (x ⊗ₜ[R] y)) =
      HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                  ((((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] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            (x ⊗ₜ[R] y) :
          A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              (x ⊗ₜ[R] y)) :
          A ⊗[R] M)
⊢ (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] M) → A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        z) =
    HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                ((((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] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          z :
        A ⊗[R] M)
      ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) :
        A ⊗[R] M)
have refine_2₂ : ∀ (x y : A ⊗[R] M),
  (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          x) =
      HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                  ((((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] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            x :
          A ⊗[R] M)
        ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              x) :
          A ⊗[R] M) →
    (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            y) =
        HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                    ((((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] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              y :
            A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                y) :
            A ⊗[R] M) →
      (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            (x + y)) =
        HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                    ((((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] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              (x + y) :
            A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                (x + y)) :
            A ⊗[R] M)
Tactic: refine z.induction_on ?_ ?_ ?_