-- Module: Mathlib.Algebra.Lie.BaseChange
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)
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)
⊢ 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)

Tactic:
refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)