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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
tmul :
  Eq (α := S ⊗[R] T) ((1 * x₁) ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂))
    ((y • x₁) ⊗ₜ[R] c)
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
    (y • x₁) ⊗ₜ[R] c
have tmul₁ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂)) ((y • x₁) ⊗ₜ[R] c)
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
-- 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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
tmul :
  Eq (α := S ⊗[R] T) ((1 * x₁) ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂))
    ((y • x₁) ⊗ₜ[R] c)
tmul₁ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂)) ((y • x₁) ⊗ₜ[R] c)
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
    (y • x₁) ⊗ₜ[R] c
have tmul₂ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂)) ((y • x₁) ⊗ₜ[R] c)
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
-- 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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
tmul :
  Eq (α := S ⊗[R] T) ((1 * x₁) ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂))
    ((y • x₁) ⊗ₜ[R] c)
tmul₁ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₂ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂)) ((y • x₁) ⊗ₜ[R] c)
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
    (y • x₁) ⊗ₜ[R] c
have tmul₃ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) ((y • x₁) ⊗ₜ[R] c)
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
-- 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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
tmul :
  Eq (α := S ⊗[R] T) ((1 * x₁) ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂))
    ((y • x₁) ⊗ₜ[R] c)
tmul₁ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₂ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₃ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) ((y • x₁) ⊗ₜ[R] c)
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
    (y • x₁) ⊗ₜ[R] c
have tmul₄ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) (x₁ ⊗ₜ[R] (y • c))
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
-- 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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
tmul :
  Eq (α := S ⊗[R] T) ((1 * x₁) ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂))
    ((y • x₁) ⊗ₜ[R] c)
tmul₁ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₂ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₃ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) ((y • x₁) ⊗ₜ[R] c)
tmul₄ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) (x₁ ⊗ₜ[R] (y • c))
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
    (y • x₁) ⊗ₜ[R] c
have tmul₅ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T))
  (x₁ ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) y : T) c)
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
-- 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₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
tmul :
  Eq (α := S ⊗[R] T) ((1 * x₁) ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂))
    ((y • x₁) ⊗ₜ[R] c)
tmul₁ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₂ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₃ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) ((y • x₁) ⊗ₜ[R] c)
tmul₄ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) (x₁ ⊗ₜ[R] (y • c))
tmul₅ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T))
    (x₁ ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) y : T) c)
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
    (y • x₁) ⊗ₜ[R] c
have tmul₆ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) y : T) c)
  (x₁ ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) y : T) c)
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
-- 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
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
have add : ∀ (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), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
Tactic: obtain ⟨t₁, r₁, a₁, hr₁, e₁⟩ := hx₁
Cleared hypotheses: hx₁
-- 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
hx₂ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 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₁
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
have add : ∀ (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), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
Tactic: obtain ⟨t₂, r₂, a₂, hr₂, e₂⟩ := hx₂
Cleared hypotheses: hx₂
-- 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₂
⊢ (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
have simp_rw : (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂
Tactic: simp_rw [← smul_eq_mul]
-- 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₂
⊢ (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂
have rw : (r₁ • t₁) • r₂ • t₂ = (r₁ • t₁) • r₂ • t₂
Tactic: rw [smul_smul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (hypothesis)
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₂
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
have this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
Tactic: have : (r₁ * r₂) • (t₁ * t₂) = (r₁ • t₁) * (r₂ • t₂) := by
      simp_rw [← smul_eq_mul]; rw [smul_smul_smul_comm]
-- 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₂
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
have add : 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
Tactic: refine ⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩
-- 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₂
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have add : 1 ⊗ₜ[R] (r₁ • t₁ * r₂ • t₂) * (x₁ + 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have add₁ : HMul.hMul (α := S) 1 1 ⊗ₜ[R] (r₁ • t₁ * r₂ • t₂) * (x₁ + 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have add₂ : HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r₁ • t₁)) (1 ⊗ₜ[R] (r₂ • t₂)) * (x₁ + 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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂)
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
have 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₂)
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₂]