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