-- Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal A
x : A ⊗[R] B
hx :
  x ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)))) :
      Set (A ⊗[R] B))
a :
  ∀ (x : A ⊗[R] B) (h : Membership.mem (γ := Set (A ⊗[R] B)) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A)) x),
    ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
      (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          y =
        x
a₁ :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    Eq (α := A ⊗[R] B)
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          y :
        A ⊗[R] B)
      (0 : A ⊗[R] B)
a₂ :
  ∀ (x y : A ⊗[R] B)
    (hx :
      Membership.mem (γ := Submodule (A ⊗[R] B) (A ⊗[R] B))
        (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A))) x)
    (hy :
      Membership.mem (γ := Submodule (A ⊗[R] B) (A ⊗[R] B))
        (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A))) y),
    (∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
        (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            y =
          x) →
      (∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
          (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
              y_1 =
            y) →
        ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
          (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
              y_1 =
            x + y
a₃ :
  ∀ (a x : A ⊗[R] B)
    (hx :
      Membership.mem (γ := Submodule (A ⊗[R] B) (A ⊗[R] B))
        (Submodule.span (A ⊗[R] B) ((⇑includeLeft : (a : A) → A ⊗[R] B) '' (↑I : Set A))) x),
    (∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
        (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            y =
          x) →
      ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
        (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            y =
          a • x
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B),
    (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
        y =
      x

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hx