mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I ≤ Ideal.span {map (algebraMap R P.ResidueField) r}

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I ≤ Ideal.span {map (algebraMap R P.ResidueField) r}
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → id (IsLocallyArtinian X)
hY : ¬∃ R, Y = Spec R
⊢ id (IsLocallyArtinian X)

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
⊢ id (IsLocallyArtinian X)

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → id (IsLocallyArtinian X)
hY : ¬∃ R, Y = Spec R
⊢ id (IsLocallyArtinian X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → id (IsLocallyArtinian X)
hY : ¬∃ R, Y = Spec R
⊢ id (IsLocallyArtinian X)

Tactic:
exact (isLocallyArtinian_iff_openCover (Y.affineCover.pullback₁ f)).mpr fun i ↦
      this (pullback.snd _ _) ⟨_, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ 1 ⊗ₜ[R] s ∈ Q.primeCompl

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ φ₃ (IsLocalization.mk' (Localization.AtPrime Q) (1 ⊗ₜ[R] x) ⟨1 ⊗ₜ[R] s, ?refine_1⟩) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) (IsLocalization.mk' Sq x ⟨s, hs⟩)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ 1 ⊗ₜ[R] s ∈ Q.primeCompl
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → (∃ S, X = Spec S) → id (IsLocallyArtinian X)
hX : ¬∃ S, X = Spec S
⊢ id (IsLocallyArtinian X)

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
hX : ∃ S, X = Spec S
⊢ id (IsLocallyArtinian X)

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → (∃ S, X = Spec S) → id (IsLocallyArtinian X)
hX : ¬∃ S, X = Spec S
⊢ id (IsLocallyArtinian X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → id (IsFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (IsFinite f)

pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
⊢ id (IsFinite f)

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → id (IsFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (IsFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian (Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
    [IsLocallyArtinian (Spec R)], (∃ S, X = Spec S) → id (IsFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (IsFinite f)

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian (Spec R)
hX : ∃ S, X = Spec S
⊢ id (IsFinite f)

Tactic:
·

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian (Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
    [IsLocallyArtinian (Spec R)], (∃ S, X = Spec S) → id (IsFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (IsFinite f)
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ φ₃ (IsLocalization.mk' (Localization.AtPrime Q) (1 ⊗ₜ[R] x) ⟨1 ⊗ₜ[R] s, ⋯⟩) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) (IsLocalization.mk' Sq x ⟨s, hs⟩)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ φ₃ (IsLocalization.mk' (Localization.AtPrime Q) (1 ⊗ₜ[R] x) ⟨1 ⊗ₜ[R] s, ⋯⟩) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) (IsLocalization.mk' Sq x ⟨s, hs⟩)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)

pp: X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
hY : ∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
hX : ∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

Tactic:
·

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
⊢ WeaklyQuasiFiniteAt R q

Tactic:
by
  rw [Algebra.weaklyQuasiFiniteAt_iff]
  let Sq := Localization.AtPrime q
  let := Localization.AtPrime.algebraOfLiesOver p q
  let φ₁ : p.ResidueField →ₐ[R] Sq ⧸ p.map (algebraMap R Sq) :=
    Ideal.quotientMapₐ _ (IsScalarTower.toAlgHom _ _ _) (by
    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, Ideal.map_le_iff_le_comap,
      ← Ideal.comap_coe (F := AlgHom _ _ _), Ideal.comap_comap]
    simpa [← IsScalarTower.algebraMap_eq] using Ideal.le_comap_map)
  let φ₂ : p.Fiber S →ₐ[R] Sq ⧸ p.map (algebraMap R Sq) :=
    Algebra.TensorProduct.lift φ₁ (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _
  let φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ p.map (algebraMap R Sq) :=
    IsLocalization.liftAlgHom (M := Q.primeCompl) (f := φ₂) <| by
      rintro ⟨y, hy⟩
      obtain ⟨r, hrp, s, H⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ y
      suffices IsUnit (φ₂ (1 ⊗ₜ s)) by
        rw [← H, map_smul, Algebra.smul_def, IsUnit.mul_iff] at this
        exact this.2
      suffices s ∉ q by
        have := (IsLocalization.map_units (M := q.primeCompl) Sq ⟨_, this⟩).map
          (algebraMap _ (Sq ⧸ p.map (algebraMap R Sq)))
        simpa [φ₂, ← IsScalarTower.algebraMap_apply] using this
      suffices algebraMap _ _ r * y ∉ Q by simpa [← hQ, ← H, Algebra.smul_def]
      refine Q.primeCompl.mul_mem ?_ hy
      simpa only [Ideal.mem_primeCompl_iff, ← Ideal.mem_comap, ← Q.over_def p]
  have : Function.Surjective φ₃ := by
    intro x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
    refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩
    · simpa [← hQ] using hs
    · simp [φ₃, IsLocalization.lift_mk'_spec, φ₂, IsScalarTower.algebraMap_apply S Sq (Sq ⧸ _),
        -Ideal.Quotient.mk_algebraMap, ← map_mul]
  have inst : QuasiFiniteAt R Q := .trans _ p.ResidueField _
  obtain rfl := q.over_def p
  exact .of_surjective_algHom φ₃ this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) → ∃ V f, S.arrows f ∧ x ∈ V.toOpens

pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Tactic:
·

Goal state after:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) → ∃ V f, S.arrows f ∧ x ∈ V.toOpens
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Tactic:
·

Goal state after:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case refine_1
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } } → P { down := { down := ⋯ } }

pp: case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ P { down := { down := ⋯ } } → U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Tactic:
·

Goal state after:
case refine_1
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } } → P { down := { down := ⋯ } }
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ P { down := { down := ⋯ } } → U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Tactic:
·

Goal state after:
case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ P { down := { down := ⋯ } } → U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

pp: case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
·

Goal state after:
case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
·

Goal state after:
case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case refine_1
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ U.presieveOfSections s { down := { down := ⋯ } } →
    Presieve.ofArrows (fun i ↦ U.basicOpen ↑i) (fun i ↦ homOfLE ⋯) { down := { down := ⋯ } }

pp: case refine_2
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ Presieve.ofArrows (fun i ↦ U.basicOpen ↑i) (fun i ↦ homOfLE ⋯) { down := { down := ⋯ } } →
    U.presieveOfSections s { down := { down := ⋯ } }

Tactic:
·

Goal state after:
case refine_1
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ U.presieveOfSections s { down := { down := ⋯ } } →
    Presieve.ofArrows (fun i ↦ U.basicOpen ↑i) (fun i ↦ homOfLE ⋯) { down := { down := ⋯ } }
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).left

pp: case refine_2
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).right

pp: case refine_3
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Iso.hom ?refine_1 ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).hom =
    (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).hom ≫ Iso.hom ?refine_2

Tactic:
·

Goal state after:
case refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).left
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))

pp: case refine_1.refine_2
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Spec R).fromSpecResidueField x ≫ 𝟙 (Spec R) =
    Spec.map (Spec.residueFieldIso R x).inv ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))

Tactic:
·

Goal state after:
case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))