awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
    {{ asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
⊢ x ∉ q
have this₁ : r ∉ { asIdeal := qF.asIdeal, isPrime := sorry : PrimeSpectrum (p.Fiber S) }.asIdeal
Tactic: have : r ∉ _ := hrq.ge rfl
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
    {{ asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
have this₁ : x ∉ q
Tactic: have : x ∉ q := by
    have : r ∉ _ := hrq.ge rfl
    simp only [PrimeSpectrum.preimageHomeomorphFiber, PrimeSpectrum.preimageOrderIsoFiber,
      Homeomorph.homeomorph_mk_coe, qF, e] at this
    rw [PrimeSpectrum.preimageEquivFiber_apply_asIdeal,
        ← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ s), ← Algebra.smul_def, hsx] at this
    · simpa using this
    · simpa [IsScalarTower.algebraMap_apply R S q.ResidueField, q.over_def p] using hs
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
    {{ asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : x ∉ q
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
have refine : ∀ (q' : Ideal S), q'.IsPrime → ∀ (hq' : q' ≠ q), q'.LiesOver p → ∀ (hxq' : x ∉ q'), q' = q
Tactic: refine ⟨x, this, fun q' _ hq' _ ↦ not_not.mp fun hxq' ↦ hq' ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
    {{ asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : x ∉ q
q' : Ideal S
h : q'.IsPrime
hq' : q' ≠ q
h_1 : q'.LiesOver p
hxq' : x ∉ q'
⊢ q' = q
have refine : Membership.mem (α := PrimeSpectrum (p.Fiber S)) (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S)))
  ((e :
        (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := sorry }}) : Type u_2)) →
          PrimeSpectrum ({ asIdeal := p, isPrime := sorry }.asIdeal.Fiber S))
      (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := sorry : PrimeSpectrum R }})
          x)
        { asIdeal := q', isPrime := h } sorry) :
    PrimeSpectrum ({ asIdeal := p, isPrime := sorry : PrimeSpectrum R }.asIdeal.Fiber S))
Tactic: refine congr($(e.injective (a₁ := ⟨⟨q', ‹_›⟩, PrimeSpectrum.ext (q'.over_def p).symm⟩)
    (a₂ := ⟨⟨q, ‹_›⟩, PrimeSpectrum.ext (q.over_def p).symm⟩) (hrq.le ?_)).1.1)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : EssFiniteType R S
inst_7 : QuasiFiniteAt R q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }}) :
    Type u_2) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) :=
  (e :
      (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
        PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
    (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := q, isPrime := inst_4 } ⋯)
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S))) =
    {{ asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : x ∉ q
q' : Ideal S
h : q'.IsPrime
hq' : q' ≠ q
h_1 : q'.LiesOver p
hxq' : x ∉ q'
⊢ Membership.mem (α := PrimeSpectrum (p.Fiber S)) (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (p.Fiber S)))
    ((e :
          (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_2)) →
            PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
            x)
          { asIdeal := q', isPrime := h } ⋯) :
      PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber S))
have simp : r ∉
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := sorry } :
        (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := sorry }}) : Type u_2)) →
          PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {{ asIdeal := p, isPrime := sorry : PrimeSpectrum R }})
          x)
        { asIdeal := q', isPrime := h } sorry))
Tactic: simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.preimageHomeomorphFiber,
    PrimeSpectrum.preimageOrderIsoFiber, Homeomorph.homeomorph_mk_coe, Set.mem_compl_iff,
    PrimeSpectrum.mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe, e]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
⊢ Function.Surjective (α := p.ResidueField ⊗[R] S) (β := q.ResidueField)
    (⇑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯ :
          p.ResidueField ⊗[R] S →ₐ[p.ResidueField] q.ResidueField) :
      (a : p.ResidueField ⊗[R] S) → q.ResidueField)
have hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
Tactic: have hq' : q = q'.comap Algebra.TensorProduct.includeRight.toRingHom :=
    congr($((PrimeSpectrum.primesOverOrderIsoFiber R S p).symm_apply_apply ⟨q, ‹_›, ‹_›⟩).1).symm
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
⊢ Function.Surjective (α := p.ResidueField ⊗[R] S) (β := q.ResidueField)
    (⇑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯ :
          p.ResidueField ⊗[R] S →ₐ[p.ResidueField] q.ResidueField) :
      (a : p.ResidueField ⊗[R] S) → q.ResidueField)
have this : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
Tactic: have : Algebra.QuasiFiniteAt p.ResidueField q' := .baseChange q _ hq'
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
this : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
⊢ Function.Surjective (α := p.ResidueField ⊗[R] S) (β := q.ResidueField)
    (⇑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯ :
          p.ResidueField ⊗[R] S →ₐ[p.ResidueField] q.ResidueField) :
      (a : p.ResidueField ⊗[R] S) → q.ResidueField)
have this₁ : q'.IsMaximal
Tactic: have : q'.IsMaximal := (PrimeSpectrum.isClosed_singleton_iff_isMaximal _).mp
    (QuasiFiniteAt.isClopen_singleton (R := p.ResidueField) _).isClosed
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
this : q'.IsMaximal
⊢ Function.Surjective (α := p.ResidueField ⊗[R] S) (β := q.ResidueField)
    (⇑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯ :
          p.ResidueField ⊗[R] S →ₐ[p.ResidueField] q.ResidueField) :
      (a : p.ResidueField ⊗[R] S) → q.ResidueField)
have refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine .of_comp_left ?_
    (p.surjectiveOnStalks_residueField.baseChange'.residueFieldMap_bijective q q' hq').1
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
this : q'.IsMaximal
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: convert! q'.algebraMap_residueField_surjective
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
this : q'.IsMaximal
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
inst_8 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S p : (a : (↑(p.primesOver S) : Type u_2)) → PrimeSpectrum (p.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) q ⋯))
hq' : q = Ideal.comap (F := S →+* p.ResidueField ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q'
this_1 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'
this : q'.IsMaximal
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
⊢ False
have inr : ∀
  (this :
    ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
      (hR : IsField R), False)
  (hR : ¬IsField R), False
Tactic: wlog hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
inr :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
        (hR : IsField R), False)
    (hR : ¬IsField R), False
⊢ False
have wlog : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
  (hR : IsField R), False
Tactic: wlog hR : IsField R
Cleared hypotheses: P, inst_1, H
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
    (hR : IsField R), False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
⊢ False
have inr : ∀ (Q : PrimeSpectrum ({ asIdeal := p, isPrime := sorry : PrimeSpectrum R }.asIdeal.Fiber R[X]))
  (hQ :
    (Equiv.symm (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := sorry }) :
          (a : PrimeSpectrum ({ asIdeal := p, isPrime := sorry }.asIdeal.Fiber R[X])) →
            (↑(PrimeSpectrum.comap (algebraMap R R[X]) ⁻¹' {{ asIdeal := p, isPrime := sorry }}) : Type u_1))
        Q =
      Subtype.mk (p := fun (x : PrimeSpectrum R[X]) ↦
        Membership.mem (γ := Set (PrimeSpectrum R[X]))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R R[X]))
            {{ asIdeal := p, isPrime := sorry : PrimeSpectrum R }})
          x)
        { asIdeal := P, isPrime := inst_1 : PrimeSpectrum R[X] } sorry),
  False
Tactic: obtain ⟨Q, hQ⟩ := (PrimeSpectrum.preimageEquivFiber R R[X]
        ⟨p, inferInstance⟩).symm.surjective ⟨⟨P, ‹_›⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
inst_1 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_2 : P.IsPrime] (H : Algebra.WeaklyQuasiFiniteAt R P)
    (hR : IsField R), False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.Fiber R[X])
hQ :
  (Equiv.symm (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := ⋯ }) :
        (a : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber R[X])) →
          (↑(PrimeSpectrum.comap (algebraMap R R[X]) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) : Type u_1))
      Q =
    Subtype.mk (p := fun (x : PrimeSpectrum R[X]) ↦
      Membership.mem (γ := Set (PrimeSpectrum R[X]))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R R[X]))
          {{ asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }})
        x)
      { asIdeal := P, isPrime := inst_1 : PrimeSpectrum R[X] } ⋯
⊢ False
have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal
Tactic: have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal :=
      .baseChange P Q.asIdeal congr($(hQ.symm).1.1)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (hypothesis)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
P : Ideal R[X]
inst_2 : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
hR : IsField R
this : Field R := hR.toField
⊢ False
have this₁ : Module.Finite R R[X]
Tactic: have := Module.Finite.of_injective
    (IsScalarTower.toAlgHom R R[X] (Localization.AtPrime P)).toLinearMap
    (IsLocalization.injective _ P.primeCompl_le_nonZeroDivisors)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Algebra.WeaklyQuasiFiniteAt R P
algInst : Algebra.{u_1, u_2} R[X] S := f.toAlgebra
⊢ LT.lt (α := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C (Ideal.under R P))
    (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P)
have refine_1 : LE.le (α := Ideal R) (Ideal.under R P)
  (Ideal.comap (F := R →+* R[X]) C (Ideal.comap (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S) P))
Tactic: refine lt_of_le_of_ne (Ideal.map_le_iff_le_comap.mpr ?_) fun e ↦ ?_