-- 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 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
              (↑N : Submodule R M)) :
          Set (A ⊗[R] M)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                      (↑N : Submodule R M)) :
                  Set (A ⊗[R] M)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
refine_1 :
  ∀ (a : A) (y : L),
    Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
      (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y)
          ((Finsupp.linearCombination A
                (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                  x ∈
                    (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                          (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)))) :
              (a :
                  (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                          Set (A ⊗[R] M)) :
                      Type (max u_2 u_4)) →₀
                    A) →
                A ⊗[R] M)
            c) :
        A ⊗[R] M)
⊢ Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (⁅x,
        (Finsupp.linearCombination A
              (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                x ∈
                  (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                        (↑N : Submodule R M)) :
                    Set (A ⊗[R] M)))) :
            (a :
                (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4)) →₀
                  A) →
              A ⊗[R] M)
          c⁆ :
      A ⊗[R] M)
have refine_2 : ∀ (y z : A ⊗[R] L)
  (hy :
    Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
      (⁅y,
          (Finsupp.linearCombination A
                (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                  x ∈
                    (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                          (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)))) :
              (a :
                  (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                          Set (A ⊗[R] M)) :
                      Type (max u_2 u_4)) →₀
                    A) →
                A ⊗[R] M)
            c⁆ :
        A ⊗[R] M))
  (hz :
    Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
      (⁅z,
          (Finsupp.linearCombination A
                (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                  x ∈
                    (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                          (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)))) :
              (a :
                  (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                          Set (A ⊗[R] M)) :
                      Type (max u_2 u_4)) →₀
                    A) →
                A ⊗[R] M)
            c⁆ :
        A ⊗[R] M)),
  Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (⁅y + z,
        (Finsupp.linearCombination A
              (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                x ∈
                  (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                        (↑N : Submodule R M)) :
                    Set (A ⊗[R] M)))) :
            (a :
                (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4)) →₀
                  A) →
              A ⊗[R] M)
          c⁆ :
      A ⊗[R] M)
Tactic: refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)