awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈ (comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ : PrimeSpectrum S }).asIdeal ↔ x ∈ p.asIdeal
have refine_2 : (∃ x_1 ∈ p.asIdeal, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)) ↔ x ∈ p.asIdeal
Tactic: rw [comap_asIdeal, Ideal.mem_comap, Ideal.mem_map_iff_of_surjective f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1 ∈ p.asIdeal, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)) ↔ x ∈ p.asIdeal
have refine_2 : (∃ x_1 ∈ p.asIdeal, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)) → x ∈ p.asIdeal
Tactic: refine ⟨?_, fun hx => ⟨x, hx, rfl⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
⊢ x ∈ p.asIdeal
have refine_2 : x' - (x' - x) ∈ p.asIdeal
Tactic: rw [← sub_sub_cancel x' x]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
⊢ x' - (x' - x) ∈ p.asIdeal
have refine_2 : Membership.mem (γ := Submodule R R) (ker f) (x' - x)
Tactic: refine p.asIdeal.sub_mem hx' (hp ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
⊢ Membership.mem (γ := Submodule R R) (ker f) (x' - x)
have refine_2 : Eq.{v + 1} (α := S) ((f : (a : R) → S) (x' - x) : S) (0 : S)
Tactic: rwa [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
refine_2 : Eq.{v + 1} (α := S) ((f : (a : R) → S) (x' - x) : S) (0 : S)
⊢ Membership.mem (γ := Submodule R R) (ker f) (x' - x)
have refine_2₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S) = 0
Tactic: rwa [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Set.range (comap f) = zeroLocus (↑(ker f) : Set R)
have rw : comap f '' Set.univ = zeroLocus (↑(ker f) : Set R)
Tactic: rw [← Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ comap f '' Set.univ = zeroLocus (↑(ker f) : Set R)
have h : Eq (α := Set (PrimeSpectrum S)) Set.univ (zeroLocus (↑⊥ : Set S))
Tactic: convert! image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := Set (PrimeSpectrum S)) Set.univ (zeroLocus (↑⊥ : Set S))
have h : Eq.{v + 1} (α := Set (PrimeSpectrum S)) Set.univ Set.univ
Tactic: rw [zeroLocus_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
p : Ideal S
isPrime : p.IsPrime
⊢ (fun (x : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦
        (match (motive := (↑(zeroLocus (↑I : Set R)) : Type u) → PrimeSpectrum S) x with
          | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ } :
          PrimeSpectrum S))
      ((fun (p : PrimeSpectrum S) ↦
          (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
              Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x) (PrimeSpectrum.comap f p) ⋯ :
            { x : PrimeSpectrum R // Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x }))
        { asIdeal := p, isPrime := isPrime }) =
    { asIdeal := p, isPrime := isPrime : PrimeSpectrum S }
have simp : map f (PrimeSpectrum.comap f { asIdeal := p, isPrime := isPrime : PrimeSpectrum S }).asIdeal = p
Tactic: simp only [PrimeSpectrum.mk.injEq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
p : Ideal R
isPrime : p.IsPrime
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R))
    { asIdeal := p, isPrime := isPrime : PrimeSpectrum R }
⊢ (fun (p : PrimeSpectrum S) ↦
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x) (PrimeSpectrum.comap f p) ⋯ :
          { x : PrimeSpectrum R // Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x }))
      ((fun (x : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦
          (match (motive := (↑(zeroLocus (↑I : Set R)) : Type u) → PrimeSpectrum S) x with
            | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ } :
            PrimeSpectrum S))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x) { asIdeal := p, isPrime := isPrime }
          hp)) =
    Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x)
      { asIdeal := p, isPrime := isPrime : PrimeSpectrum R } hp
have simp : comap f (map f p) = p
Tactic: simp only [Subtype.mk.injEq, PrimeSpectrum.ext_iff, comap_asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
⊢ LE.le (α := Ideal R) (comap f a.asIdeal) (comap f b.asIdeal) ↔ a ≤ b
have rw : map f (comap f a.asIdeal) ≤ b.asIdeal ↔ a ≤ b
Tactic: rw [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective f hf,
      PrimeSpectrum.asIdeal_le_asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
rw : map f (comap f a.asIdeal) ≤ b.asIdeal ↔ a ≤ b
⊢ LE.le (α := Ideal R) (comap f a.asIdeal) (comap f b.asIdeal) ↔ a ≤ b
have rw₁ : a.asIdeal ≤ b.asIdeal ↔ a ≤ b
Tactic: rw [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective f hf,
      PrimeSpectrum.asIdeal_le_asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
rw : map f (comap f a.asIdeal) ≤ b.asIdeal ↔ a ≤ b
rw₁ : a.asIdeal ≤ b.asIdeal ↔ a ≤ b
⊢ LE.le (α := Ideal R) (comap f a.asIdeal) (comap f b.asIdeal) ↔ a ≤ b
have rw₂ : a ≤ b ↔ a ≤ b
Tactic: rw [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective f hf,
      PrimeSpectrum.asIdeal_le_asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ p ∈ Set.range (comap f) ↔ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal
have refine : Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal → p ∈ Set.range (comap f)
Tactic: refine ⟨fun ⟨q, hq⟩ ↦ by simp [← hq], ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal → p ∈ Set.range (comap f)
have rw : (∃ (q : Ideal S), q.IsPrime ∧ Ideal.comap f q = p.asIdeal) → p ∈ Set.range (comap f)
Tactic: rw [Ideal.comap_map_eq_self_iff_of_isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
have refine_1 : ∀ (h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)),
  Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
refine_1 :
  ∀ (h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
have refine_2 : ∀ (h : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p),
  Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
have refine_1 : ∀ (m : Ideal (k ⊗[R] S)) (hm : m.IsMaximal),
  Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
Tactic: obtain ⟨m, hm⟩ := Ideal.exists_maximal (k ⊗[R] S)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
have h₁ : comap (algebraMap R S)
    (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := sorry }) =
  p
Tactic: use PrimeSpectrum.comap (Algebra.TensorProduct.includeRight).toRingHom ⟨m, hm.isPrime⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ comap (algebraMap R S)
      (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := ⋯ }) =
    p
have h₁ : asIdeal
    (comap (algebraMap R S)
      (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := sorry })) =
  p.asIdeal
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ asIdeal
      (comap (algebraMap R S)
        (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := ⋯ })) =
    p.asIdeal
have h₁ : asIdeal
    (comap (algebraMap R k)
      (comap (S := k ⊗[R] S) Algebra.TensorProduct.includeLeftRingHom { asIdeal := m, isPrime := sorry })) =
  p.asIdeal
Tactic: rw [← PrimeSpectrum.comap_comp_apply,
      ← Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap, comap_comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
have refine_2 : ∀ (q : PrimeSpectrum S), Nontrivial (Ideal.ResidueField (asIdeal (comap (algebraMap R S) q)) ⊗[R] S)
Tactic: obtain ⟨q, rfl⟩ := h
Cleared hypotheses: p, k, h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u_1
inst : CommRing R
I : PrimeSpectrum R
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.range (ι := PrimeSpectrum I.asIdeal.ResidueField) (comap (algebraMap R I.asIdeal.ResidueField))) {I}
have rw : comap (S := I.asIdeal.ResidueField) (algebraMap R I.asIdeal.ResidueField) default = I
Tactic: rw [Set.range_unique, Set.singleton_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
⊢ IsUnit x
have by_contra : ∀ (hx : ¬IsUnit x), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
⊢ False
have obtain : ∀ (p : Ideal R) (hp : p.IsMaximal), x ∈ p → False
Tactic: obtain ⟨p, hp, _⟩ := exists_max_ideal_of_mem_nonunits hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right : x ∈ p
⊢ False
have obtain : ∀ (q : Ideal S) (hqp : q.IsPrime)
  (hq : comap f { asIdeal := q, isPrime := hqp : PrimeSpectrum S } = { asIdeal := p, isPrime := sorry }), False
Tactic: obtain ⟨⟨q, hqp⟩, hq⟩ := hf ⟨p, hp.isPrime⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : comap f { asIdeal := q, isPrime := hqp : PrimeSpectrum S } = { asIdeal := p, isPrime := ⋯ }
⊢ False
have hq₁ : Ideal.comap f q = p
Tactic: simp only [PrimeSpectrum.ext_iff, comap_asIdeal] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
⊢ x ∈ p₂.asIdeal
have by_contra : ∀ (hxp₂ : x ∉ p₂.asIdeal), False
Tactic: by_contra hxp₂
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
⊢ False
have obtain : ∀ (t : T) (r : R) (a : S) (ht : r • t ∉ Ideal.comap g p₂.asIdeal) (e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t), False
Tactic: obtain ⟨t, r, a, ht, e⟩ := hRT.exists_mul_eq_tmul x
    (p₂.asIdeal.comap g) inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ False
have h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
Tactic: have h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal := e ▸ p₁.asIdeal.mul_mem_left (1 ⊗ₜ[R] (r • t)) hxp₁
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
⊢ False
have h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal
Tactic: have h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal := e ▸ p₂.asIdeal.primeCompl.mul_mem ht hxp₂
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal
⊢ False
have h₃ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
Tactic: rw [← mul_one a, ← one_mul t, ← Algebra.TensorProduct.tmul_mul_tmul] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal
h₃ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
⊢ False
have h₄ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
Tactic: rw [← mul_one a, ← one_mul t, ← Algebra.TensorProduct.tmul_mul_tmul] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
h₂ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
⊢ False
have h₃ : t ∉ Ideal.comap g p₂.asIdeal
Tactic: have h₃ : t ∉ p₂.asIdeal.comap g := fun h ↦ h₂ (Ideal.mul_mem_left _ _ h)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
h₂ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
⊢ False
have h₄ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₂.asIdeal
Tactic: have h₄ : a ∉ p₂.asIdeal.comap (algebraMap S (S ⊗[R] T)) :=
    fun h ↦ h₂ (Ideal.mul_mem_right _ _ h)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
h₂ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
h₄ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₂.asIdeal
⊢ False
have h₅ : t ∉ Ideal.comap g p₁.asIdeal
Tactic: replace h₃ : t ∉ p₁.asIdeal.comap g := by
    rwa [show p₁.asIdeal.comap g = p₂.asIdeal.comap g from congr($h.2.1)]
Cleared hypotheses: h₃