-- 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_1 : A ⊗[R] B
hx :
  x_1 ∈
    (↑(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))
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
a : A
b : B
a₁ :
  ∃ (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 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          0)
a₂ :
  ∀ (x : ↥(Submodule.restrictScalars R I)) (y : B),
    ∃ (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 =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
              (x ⊗ₜ[R] y) :
            A ⊗[R] B)
a₃ :
  ∀ (x y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
    (hx :
      ∃ (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 =
          HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
            ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                  (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
                x :
              A ⊗[R] B))
    (hy :
      ∃ (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 =
          HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (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)),
    ∃ (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 =
        HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
          ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
              (x + y) :
            A ⊗[R] B)
⊢ ∃ (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 =
      HSMul.hSMul (α := A ⊗[R] B) (β := A ⊗[R] B) (a ⊗ₜ[R] b)
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → 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 [smul_eq_mul]
          with_unfolding_all 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, MulZeroClass.mul_zero, HSMul.hSMul, smul_eq_mul, smul_add