-- 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)
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)
have refine_2 : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
  (HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[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)
    (⁅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: rw [add_lie]