awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
hR : R ∈ (etaleTopology : (a : Scheme) → Set (Sieve a)) S
f : Spec (CommRingCat.of Ω) ⟶ S
obtain :
  ∀ (x : ↥S) (a : S.residueField x ⟶ CommRingCat.of Ω),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y :
      Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
              (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
                (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
            y :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((Equiv.symm (SpecToEquivOfField Ω S) :
              (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
            (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) x a) :
          Spec (CommRingCat.of Ω) ⟶ S)
⊢ ∃ (Y : Scheme.{u}) (f_1 : Y ⟶ S) (_ : R.arrows f_1) (y :
    Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f_1) :
          (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
            (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
        y =
      f

Tactic:
obtain ⟨⟨x, a⟩, rfl⟩ := (Scheme.SpecToEquivOfField Ω S).symm.surjective f

Premises used: AlgebraicGeometry.Scheme.SpecToEquivOfField, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
hR : R ∈ (etaleTopology : (a : Scheme) → Set (Sieve a)) S
x : ↥S
a : S.residueField x ⟶ CommRingCat.of Ω
rw :
  ∀ (hR : ∃ (𝒰 : Cover (precoverage @Etale) S), Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows) (x : ↥S)
    (a : S.residueField x ⟶ CommRingCat.of Ω),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y :
      Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
              (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
                (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
            y :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((Equiv.symm (SpecToEquivOfField Ω S) :
              (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
            (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) x a) :
          Spec (CommRingCat.of Ω) ⟶ S)
⊢ ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y :
    Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) x a) :
        Spec (CommRingCat.of Ω) ⟶ S)

Tactic:
rw [mem_grothendieckTopology_iff] at hR

Premises used: AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
hR : ∃ (𝒰 : Cover (precoverage @Etale) S), Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
x : ↥S
a : S.residueField x ⟶ CommRingCat.of Ω
obtain :
  ∀ (𝒰 : Cover (precoverage @Etale) S) (hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y :
      Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
              (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
                (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
            y :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((Equiv.symm (SpecToEquivOfField Ω S) :
              (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
            (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) x a) :
          Spec (CommRingCat.of Ω) ⟶ S)
⊢ ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y :
    Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) x a) :
        Spec (CommRingCat.of Ω) ⟶ S)

Tactic:
obtain ⟨𝒰, hle⟩ := hR
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
x : ↥S
a : S.residueField x ⟶ CommRingCat.of Ω
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
obtain :
  ∀ (i : 𝒰.I₀) (y : ↥(𝒰.X i)) (a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y_1 :
      Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
              (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
                (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
            y_1 :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
        ((Equiv.symm (SpecToEquivOfField Ω S) :
              (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
            (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
              (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
          Spec (CommRingCat.of Ω) ⟶ S)
⊢ ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y :
    Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) x a) :
        Spec (CommRingCat.of Ω) ⟶ S)

Tactic:
obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
⊢ ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y_1 :
    Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y_1 :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
            (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
        Spec (CommRingCat.of Ω) ⟶ S)

Tactic:
⟨𝒰.X i, 𝒰.f i, hle _ _ ⟨i⟩, ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.PreZeroHypercover.X, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
refine :
  ∃ (y_1 : Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.X i)),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.f i)) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj (𝒰.X i))) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y_1 :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
            (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
        Spec (CommRingCat.of Ω) ⟶ S)
⊢ ∃ (Y : Scheme.{u}) (f : Y ⟶ S) (_ : R.arrows f) (y_1 :
    Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) Y),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) f) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj Y)) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y_1 :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
            (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
        Spec (CommRingCat.of Ω) ⟶ S)

Tactic:
refine ⟨𝒰.X i, 𝒰.f i, hle _ _ ⟨i⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
hf : CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom) = CommRingCat.Hom.hom a
⊢ Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
⊢ CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom) = CommRingCat.Hom.hom a

Tactic:
b.comp_algebraMap

Premises used: AlgHom.comp_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
⊢ CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom) = CommRingCat.Hom.hom a

Tactic:
exact b.comp_algebraMap

Premises used: AlgHom.comp_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
⊢ Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a

Tactic:
have hfac : (𝒰.f i).residueFieldMap y ≫ CommRingCat.ofHom b.toRingHom = a := by
      ext1; exact b.comp_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
hfac : Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.f i)) :
          (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj (𝒰.X i))) →
            (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
        (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ (𝒰.X i).fromSpecResidueField y) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
    ((Equiv.symm (SpecToEquivOfField Ω S) :
          (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
        (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
          (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
      Spec (CommRingCat.of Ω) ⟶ S)

Tactic:
simp [SpecToEquivOfField, ← hfac]

Premises used: AlgebraicGeometry.Scheme.SpecToEquivOfField
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ zariskiPrecoverage ≤ fppfPrecoverage

Tactic:
precoverage_mono fun _ _ _ _ ↦ ⟨inferInstance, inferInstance⟩

Premises used: AlgebraicGeometry.Scheme.precoverage_mono, inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fppfPrecoverage = precoverage @Flat ⊓ precoverage @LocallyOfFinitePresentation

Tactic:
grind [fppfPrecoverage, precoverage, precoverage, MorphismProperty.precoverage_inf]

Premises used: AlgebraicGeometry.Scheme.fppfPrecoverage, CategoryTheory.MorphismProperty.precoverage_inf, AlgebraicGeometry.Scheme.precoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
rw : fppfPrecoverage ≤ qcPrecoverage ∧ fppfPrecoverage ≤ precoverage @Flat
⊢ fppfPrecoverage ≤ fpqcPrecoverage

Tactic:
rw [fpqcPrecoverage, propQCPrecoverage, le_inf_iff]

Premises used: AlgebraicGeometry.Scheme.propQCPrecoverage, le_inf_iff, AlgebraicGeometry.Scheme.fpqcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fppfPrecoverage ≤ qcPrecoverage ∧ fppfPrecoverage ≤ precoverage @Flat

Tactic:
⟨?_, precoverage_mono fun X Y f ⟨hf, _⟩ ↦ inferInstance⟩

Premises used: AlgebraicGeometry.Flat, _private.0.AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage.match_2, AlgebraicGeometry.Scheme.precoverage_mono, inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
refine : fppfPrecoverage ≤ qcPrecoverage
⊢ fppfPrecoverage ≤ qcPrecoverage ∧ fppfPrecoverage ≤ precoverage @Flat

Tactic:
refine ⟨?_, precoverage_mono fun X Y f ⟨hf, _⟩ ↦ inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fppfPrecoverage ≤ qcPrecoverage

Tactic:
precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f ⟨_, _⟩ ↦ f.isOpenMap

Premises used: _private.0.AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage.match_2, CategoryTheory.ConcreteCategory.hom, IsOpenMap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.isOpenMap, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fppfPrecoverage ≤ qcPrecoverage

Tactic:
exact precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f ⟨_, _⟩ ↦ f.isOpenMap

Premises used: AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ zariskiPrecoverage ≤ fpqcPrecoverage

Tactic:
le_trans zariskiPrecoverage_le_fppfPrecoverage fppfPrecoverage_le_fpqcPrecoverage

Premises used: AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fppfPrecoverage, le_trans
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fpqcTopology = propQCTopology @Flat

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.fpqcPrecoverage, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ zariskiTopology ≤ fpqcTopology

Tactic:
Precoverage.toGrothendieck_mono zariskiPrecoverage_le_fpqcPrecoverage

Premises used: CategoryTheory.Precoverage.toGrothendieck_mono, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fpqcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fppfTopology ≤ fpqcTopology

Tactic:
Precoverage.toGrothendieck_mono fppfPrecoverage_le_fpqcPrecoverage

Premises used: CategoryTheory.Precoverage.toGrothendieck_mono, AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fpqcTopology.Subcanonical

Tactic:
GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ fun X ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
refine : ∀ (X : Scheme.{u_1}), Presieve.IsSheaf fpqcTopology (Functor.obj yoneda X)
⊢ fpqcTopology.Subcanonical

Tactic:
refine GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ fun X ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
rw :
  Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))
⊢ Presieve.IsSheaf fpqcTopology (Functor.obj yoneda X)

Tactic:
rw [fpqcTopology_eq_propQCTopology, isSheaf_type_propQCTopology_iff]

Premises used: AlgebraicGeometry.isSheaf_type_propQCTopology_iff, AlgebraicGeometry.Scheme.fpqcTopology_eq_propQCTopology