-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
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)
⊢ ∃ (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)
have 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)
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']
Cleared hypotheses: x