-- 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
refine_1 :
  ((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) 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) 0 : (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) 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) 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) 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) x : 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) x : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) :
        A ⊗[R] M)
have refine_2 : ∀ (x : A) (y_1 : L),
  (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (x ⊗ₜ[R] y_1) : 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) (x ⊗ₜ[R] y_1) :
                      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) (x ⊗ₜ[R] y_1) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) :
        A ⊗[R] M)
Tactic: refine x.induction_on ?_ ?_ ?_