-- 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₁ :
  ∀ (x y : A ⊗[R] L) (z : 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] 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)))
          y →
        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)))
            z →
          Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x, z⁆ →
            Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅y, z⁆ →
              Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x + y, z⁆
⊢ ∀ (x y : A ⊗[R] L) (z : 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] 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)))
        y)
    (hz :
      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)))
        z),
    (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 z hx hz →
      (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⁆)
          y z hy hz →
        (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) z ⋯ hz

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

Premises used: AddMemClass.add_mem, Submodule.smul_mem