awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
obtain :
  ∀ (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 ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'

Tactic:
obtain ⟨r, hr, hrq⟩ := Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton
    (R := p.ResidueField) qF.asIdeal

Premises used: Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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) }}
obtain :
  ∀ (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'
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'

Tactic:
obtain ⟨s, hs, x, hsx⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ r

Premises used: Ideal.Fiber.exists_smul_eq_one_tmul
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
⊢ r ∉ { asIdeal := qF.asIdeal, isPrime := ⋯ : PrimeSpectrum (p.Fiber S) }.asIdeal

Tactic:
have : r ∉ _ := hrq.ge rfl
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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

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
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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'

Tactic:
⟨x, this, fun q' _ hq' _ ↦ not_not.mp fun hxq' ↦ hq' ?_⟩

Premises used: Classical.not_not, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
refine : ∀ (q' : Ideal S), q'.IsPrime → ∀ (hq' : q' ≠ q), q'.LiesOver p → ∀ (hxq' : x ∉ q'), q' = q
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'

Tactic:
refine ⟨x, this, fun q' _ hq' _ ↦ not_not.mp fun hxq' ↦ hq' ?_⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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

Tactic:
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)

Premises used: congrArg, id, Eq.le, Homeomorph.injective, Subtype.val, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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'
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 := ⋯ }}) : 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))
⊢ q' = q

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)
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 ⋯))
⊢ 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
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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'
⊢ QuasiFiniteAt p.ResidueField (S := p.Fiber S) q'

Tactic:
have : Algebra.QuasiFiniteAt p.ResidueField q' := .baseChange q _ hq'
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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'
⊢ q'.IsMaximal

Tactic:
have : q'.IsMaximal := (PrimeSpectrum.isClosed_singleton_iff_isMaximal _).mp
    (QuasiFiniteAt.isClopen_singleton (R := p.ResidueField) _).isClosed
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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)

Tactic:
.of_comp_left ?_
    (p.surjectiveOnStalks_residueField.baseChange'.residueFieldMap_bijective q q' hq').1

Premises used: Ideal.surjectiveOnStalks_residueField, Function.Surjective.of_comp_left, RingHom.SurjectiveOnStalks.residueFieldMap_bijective, And.left, RingHom.SurjectiveOnStalks.baseChange'
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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)

Tactic:
refine .of_comp_left ?_
    (p.surjectiveOnStalks_residueField.baseChange'.residueFieldMap_bijective q q' hq').1
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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.Fiber S) (β := q'.ResidueField (R := p.Fiber S))
    (⇑(algebraMap (p.Fiber S) (q'.ResidueField (R := p.Fiber S))) : (a : p.Fiber S) → q'.ResidueField)

Tactic:
q'.algebraMap_residueField_surjective

Premises used: Ideal.algebraMap_residueField_surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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)

Tactic:
convert! q'.algebraMap_residueField_surjective

Premises used: Ideal.algebraMap_residueField_surjective
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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)
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)

Tactic:
ext