-- 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
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 :
  ∀ (x : A ⊗[R] L) (y : A ⊗[R] M)
    (hx :
      x ∈
        (↑(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)))
    (hy :
      y ∈
        (↑(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))),
    (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 ⋯ ⋯
refine_2₁ :
  ∀ (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
refine_2₂ :
  ∀ (x : A ⊗[R] L) (y 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] 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)
    (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 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⁆)
          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⁆)
          x (y + z) hx ⋯
⊢ ⁅x, m⁆ ∈ (↑(Submodule.span A s) : Set (A ⊗[R] M))
have refine_2₃ : ∀ (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 sorry hy
Tactic: refine Submodule.span_induction₂ (p := fun x m _ _ ↦ ⁅x, m⁆ ∈ Submodule.span A s)
      ?_ (by simp) (by simp) ?_ ?_ ?_ ?_ hx hm