-- 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
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := 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)))
    m
refine_2 refine_2₁ :
  ∀ (r : A) (x : A ⊗[R] L) (y : A ⊗[R] M),
    Membership.mem (γ := Submodule A (A ⊗[R] L))
        (Submodule.span A
          (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                (↑I : Submodule R L)) :
            Set (A ⊗[R] L)))
        x →
      Membership.mem (γ := 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)))
          y →
        Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x, y⁆ →
          Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅r • x, y⁆
⊢ ∀ (r : A) (x : A ⊗[R] L) (y : A ⊗[R] M)
    (hx :
      Membership.mem (γ := Submodule A (A ⊗[R] L))
        (Submodule.span A
          (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                (↑I : Submodule R L)) :
            Set (A ⊗[R] L)))
        x)
    (hy :
      Membership.mem (γ := 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)))
        y),
    (fun (x : A ⊗[R] L) (m : A ⊗[R] M)
            (x_1 :
              Membership.mem (γ := Submodule A (A ⊗[R] L))
                (Submodule.span A
                  (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                        (↑I : Submodule R L)) :
                    Set (A ⊗[R] L)))
                x)
            (x_2 :
              Membership.mem (γ := 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)))
                m) ↦
          Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x, m⁆)
        x y hx hy →
      (fun (x : A ⊗[R] L) (m : A ⊗[R] M)
            (x_1 :
              Membership.mem (γ := Submodule A (A ⊗[R] L))
                (Submodule.span A
                  (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                        (↑I : Submodule R L)) :
                    Set (A ⊗[R] L)))
                x)
            (x_2 :
              Membership.mem (γ := 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)))
                m) ↦
          Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x, m⁆)
        (r • x) y ⋯ hy

Tactic:
{ intros; simp [add_mem, Submodule.smul_mem, *] }

Premises used: AddMemClass.add_mem, Submodule.smul_mem