-- 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
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) 0 : (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)
                0) :
            (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) 0 : (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)
refine_2₁ :
  ∀ (x : A) (y : L),
    (((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) (x ⊗ₜ[R] y) : 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)
                    (x ⊗ₜ[R] y)) :
                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) (x ⊗ₜ[R] y) : 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)
⊢ (((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) y : 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)
                  y) :
              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) y : 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] L),
  (((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) x : 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)
                    x) :
                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) x : 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) →
    (((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) y : 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)
                      y) :
                  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) y : 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) →
      (((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) (x + y) : 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)
                      (x + y)) :
                  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) (x + y) : 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)
Tactic: refine y.induction_on ?_ ?_ ?_