-- 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
y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B
a :
  (LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
        (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
      0 ∈
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))
a₁ :
  ∀ (a : ↥(Submodule.restrictScalars R I)) (b : B),
    Membership.mem (α := A ⊗[R] B)
      (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (A ⊗[R] B))
      ((LinearMap.rTensor B (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : ↥(Submodule.restrictScalars R I) ⊗[R] B) → A ⊗[R] B)
          (a ⊗ₜ[R] b) :
        A ⊗[R] B)
a₂ :
  ∀ (x y : TensorProduct.{u_1, u_2, u_3} R (↥(Submodule.restrictScalars R I)) B)
    (hx :
      Membership.mem (α := A ⊗[R] B)
        (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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 :
      Membership.mem (α := A ⊗[R] B)
        (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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)),
    Membership.mem (α := A ⊗[R] B)
      (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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)
⊢ Membership.mem (α := A ⊗[R] B)
    (↑(Submodule.restrictScalars R (map (F := A →ₐ[R] A ⊗[R] B) includeLeft I)) : Set (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)

Tactic:
induction y with
    | zero =>
        rw [map_zero]
        apply zero_mem
    | tmul a b =>
        simp only [LinearMap.rTensor_tmul, Submodule.coe_subtype]
        suffices (a : A) ⊗ₜ[R] b = ((1 : A) ⊗ₜ[R] b) * ((a : A) ⊗ₜ[R] (1 : B)) by
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          rw [this]
          apply Ideal.mul_mem_left
          -- Note: adding `includeLeft` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeLeft
          exact Submodule.coe_mem a
        simp only [Algebra.TensorProduct.tmul_mul_tmul,
          mul_one, one_mul]
    | add x y hx hy =>
        rw [map_add]
        apply Submodule.add_mem _ hx hy

Premises used: LinearMap.rTensor_tmul, map_zero, map_add, Algebra.TensorProduct.tmul_mul_tmul, Submodule.coe_subtype, ZeroMemClass.zero_mem, mul_one, one_mul