-- 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 B
x_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(Submodule.restrictScalars R (R := A ⊗[R] B)
          (Submodule.span (A ⊗[R] B) ((⇑includeRight : (a : B) → A ⊗[R] B) '' (↑I : Set B)))) :
      Set (A ⊗[R] B))
x : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)
a : A
b : B
a₁ :
  ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          0)
a₂ :
  ∀ (x : A) (y : ↥(Submodule.restrictScalars R I)),
    ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y_1 =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              (x ⊗ₜ[R] y) :
            A ⊗[R] B)
a₃ :
  ∀ (x y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I))
    (hx :
      ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
        (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            y =
          HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
            ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                  (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
                x :
              A ⊗[R] B))
    (hy :
      ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
        (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            y_1 =
          HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
            ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                  (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
                y :
              A ⊗[R] B)),
    ∃ (y_1 : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
      (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
          y_1 =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
              (x + y) :
            A ⊗[R] B)
⊢ ∃ (y : TensorProduct.{u_1, u_2, u_3} R A ↥(Submodule.restrictScalars R I)),
    (LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
        y =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.lTensor A (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : A ⊗[R] ↥(Submodule.restrictScalars R I)) → A ⊗[R] B)
            x :
          A ⊗[R] B)

Tactic:
induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a * x) ⊗ₜ[R] (b • y)
          simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]
          rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']

Premises used: map_zero, map_add, Algebra.TensorProduct.tmul_mul_tmul, MulZeroClass.mul_zero, Submodule.coe_subtype, smul_eq_mul, smul_add, LinearMap.lTensor_tmul