-- 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))
a : A ⊗[R] B
x : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) 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) 0
        ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
            x :
          A ⊗[R] B)
a₂ :
  ∀ (a : A) (b : 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)
a₃ :
  ∀ (a b : A ⊗[R] B)
    (ha :
      ∃ (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
            ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                  (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
                x :
              A ⊗[R] B))
    (hb :
      ∃ (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) b
            ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                  (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
                x :
              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 + b)
          ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
              x :
            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
        ((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 a with
      | zero =>
        use 0
        simp only [map_zero, smul_eq_mul, zero_mul]
      | tmul a b =>
        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']
      | add a b ha hb =>
        obtain ⟨x', ha'⟩ := ha
        obtain ⟨y', hb'⟩ := hb
        use x' + y'
        simp only [map_add, ha', add_smul, hb']

Premises used: MulZeroClass.zero_mul, map_zero, map_add, MulZeroClass.mul_zero, add_smul, smul_eq_mul, smul_add