awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂]
-- 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂]
-- 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂]
-- 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂]
-- 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂]
-- 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have add₁₂ : (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + 1 ⊗ₜ[R] (r₁ • t₁) * (1 ⊗ₜ[R] (r₂ • t₂) * x₂) = (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₂]
-- 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂]
-- 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)
x : S ⊗[R] T
J : Ideal T
hJ : J.IsPrime
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
have zero : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) 0 = a ⊗ₜ[R] t
Tactic: induction x with
  | zero =>
    exact ⟨1, 1, 0, by rw [one_smul]; exact J.primeCompl.one_mem,
      by rw [mul_zero, TensorProduct.zero_tmul]⟩
  | tmul x₁ x₂ =>
    obtain ⟨y, s, c, hs, hc, e⟩ := (surjective_localRingHom_iff _).mp (hf₂ J hJ) x₂
    simp_rw [Algebra.smul_def]
    refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩
    rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
  | add x₁ x₂ hx₁ hx₂ =>
    obtain ⟨t₁, r₁, a₁, hr₁, e₁⟩ := hx₁
    obtain ⟨t₂, r₂, a₂, hr₂, e₂⟩ := hx₂
    have : (r₁ * r₂) • (t₁ * t₂) = (r₁ • t₁) * (r₂ • t₂) := by
      simp_rw [← smul_eq_mul]; rw [smul_smul_smul_comm]
    refine ⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩
    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₂]
Cleared hypotheses: x
-- 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)
x : S ⊗[R] T
J : Ideal T
hJ : J.IsPrime
zero : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) 0 = a ⊗ₜ[R] t
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
have tmul : ∀ (x₁ : S) (x₂ : T),
  ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) (x₁ ⊗ₜ[R] x₂) = a ⊗ₜ[R] t
Tactic: induction x with
  | zero =>
    exact ⟨1, 1, 0, by rw [one_smul]; exact J.primeCompl.one_mem,
      by rw [mul_zero, TensorProduct.zero_tmul]⟩
  | tmul x₁ x₂ =>
    obtain ⟨y, s, c, hs, hc, e⟩ := (surjective_localRingHom_iff _).mp (hf₂ J hJ) x₂
    simp_rw [Algebra.smul_def]
    refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩
    rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
  | add x₁ x₂ hx₁ hx₂ =>
    obtain ⟨t₁, r₁, a₁, hr₁, e₁⟩ := hx₁
    obtain ⟨t₂, r₂, a₂, hr₂, e₂⟩ := hx₂
    have : (r₁ * r₂) • (t₁ * t₂) = (r₁ • t₁) * (r₂ • t₂) := by
      simp_rw [← smul_eq_mul]; rw [smul_smul_smul_comm]
    refine ⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩
    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₂]
Cleared hypotheses: x
-- 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)
x : S ⊗[R] T
J : Ideal T
hJ : J.IsPrime
zero : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) 0 = a ⊗ₜ[R] t
tmul :
  ∀ (x₁ : S) (x₂ : T),
    ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) (x₁ ⊗ₜ[R] x₂) = a ⊗ₜ[R] t
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
have add : ∀ (x₁ x₂ : S ⊗[R] T) (hx₁ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ = a ⊗ₜ[R] t)
  (hx₂ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₂ = a ⊗ₜ[R] t),
  ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
Tactic: induction x with
  | zero =>
    exact ⟨1, 1, 0, by rw [one_smul]; exact J.primeCompl.one_mem,
      by rw [mul_zero, TensorProduct.zero_tmul]⟩
  | tmul x₁ x₂ =>
    obtain ⟨y, s, c, hs, hc, e⟩ := (surjective_localRingHom_iff _).mp (hf₂ J hJ) x₂
    simp_rw [Algebra.smul_def]
    refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩
    rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
  | add x₁ x₂ hx₁ hx₂ =>
    obtain ⟨t₁, r₁, a₁, hr₁, e₁⟩ := hx₁
    obtain ⟨t₂, r₂, a₂, hr₂, e₂⟩ := hx₂
    have : (r₁ * r₂) • (t₁ * t₂) = (r₁ • t₁) * (r₂ • t₂) := by
      simp_rw [← smul_eq_mul]; rw [smul_smul_smul_comm]
    refine ⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩
    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₂]
Cleared hypotheses: x