-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
add : 1 ⊗ₜ[R] (r₁ • t₁ * r₂ • t₂) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₁ : HMul.hMul (α := S) 1 1 ⊗ₜ[R] (r₁ • t₁ * r₂ • t₂) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₂ :
  HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₁ • t₁)) (1 ⊗ₜ[R] (r₂ • t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₃ :
  HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₁ • t₁)) (1 ⊗ₜ[R] (r₂ • t₂)) * x₁ +
      HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₁ • t₁)) (1 ⊗ₜ[R] (r₂ • t₂)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₄ :
  HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₁ +
      HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₅ :
  1 ⊗ₜ[R] (r₂ • t₂) * (1 ⊗ₜ[R] (r₁ • t₁) * x₁) +
      HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₆ :
  HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (a₁ ⊗ₜ[R] t₁) +
      HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₇ :
  (1 * a₁) ⊗ₜ[R] (r₂ • t₂ * t₁) + HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₈ :
  a₁ ⊗ₜ[R] (r₂ • t₂ * t₁) + HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₉ :
  a₁ ⊗ₜ[R] (r₂ • (t₂ * t₁)) + HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₁₀ :
  (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₂ • t₂)) (1 ⊗ₜ[R] (r₁ • t₁)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₁₁ :
  (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₁ • t₁)) (1 ⊗ₜ[R] (r₂ • t₂)) * x₂ =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₁₂ : (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + 1 ⊗ₜ[R] (r₁ • t₁) * (1 ⊗ₜ[R] (r₂ • t₂) * x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₁₃ :
  (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₁ • t₁)) (a₂ ⊗ₜ[R] t₂) =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
add₁₄ :
  HAdd.hAdd (α := S ⊗[R] T) ((r₂ • a₁) ⊗ₜ[R] (t₂ * t₁)) ((1 * a₂) ⊗ₜ[R] (r₁ • t₁ * t₂)) =
    (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have add₁₅ : HAdd.hAdd (α := S ⊗[R] T) ((r₂ • a₁) ⊗ₜ[R] (t₂ * t₁)) (a₂ ⊗ₜ[R] (r₁ • t₁ * t₂)) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
Tactic: rw [this, ← one_mul (1 : S), ← Algebra.TensorProduct.tmul_mul_tmul, mul_add, mul_comm (_ ⊗ₜ _),
      mul_assoc, e₁, Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc,
      ← TensorProduct.smul_tmul, mul_comm (_ ⊗ₜ _), mul_assoc, e₂,
      Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc, ← TensorProduct.smul_tmul,
      TensorProduct.add_tmul, mul_comm t₁ t₂]