awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
⊢ (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))
have refine_2 : ∀ (a b : ↥(Spec S))
  (hfab :
    Eq (α := ↥(Opposite.unop (Opposite.op (Spec R)))) ((Spec.map f) a : ↥(Opposite.unop (Opposite.op (Spec R))))
      ((Spec.map f) b : ↥(Opposite.unop (Opposite.op (Spec R))))),
  Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) a : T) ((x : (a : ↥(Spec S)) → T) b : T)
Tactic: refine Topology.IsQuotientMap.lift this x fun a b hfab ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
a b : ↥(Spec S)
hfab :
  Eq (α := ↥(Opposite.unop (Opposite.op (Spec R)))) ((Spec.map f) a : ↥(Opposite.unop (Opposite.op (Spec R))))
    ((Spec.map f) b : ↥(Opposite.unop (Opposite.op (Spec R))))
⊢ Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) a : T) ((x : (a : ↥(Spec S)) → T) b : T)
have refine_2 : ∀ (c : ↥(pullback (Spec.map f) (Spec.map f)))
  (hfab :
    Eq (α := ↥(Opposite.unop (Opposite.op (Spec R))))
      ((Spec.map f) ((pullback.fst (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))
      ((Spec.map f) ((pullback.snd (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))),
  Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) ((pullback.fst (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)
    ((x : (a : ↥(Spec S)) → T) ((pullback.snd (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)
Tactic: obtain ⟨c, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback a b hfab
Cleared hypotheses: a, b, hfab
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
y : (continuousMapPresheaf T).obj (Opposite.op (Spec R))
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
        (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
      y =
    x
⊢ y = this.lift x ⋯
have refine_2 : ContinuousMap.comp y
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
      (Spec.map f).base) =
  (this.lift x sorry).comp
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
      (Spec.map f).base)
Tactic: rwa [← ContinuousMap.cancel_right (Spec.map f).surjective, Topology.IsQuotientMap.lift_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
y : (continuousMapPresheaf T).obj (Opposite.op (Spec R))
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
        (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
      y =
    x
refine_2 :
  ContinuousMap.comp y
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
        TopCat.carrier) (Spec.map f).base) =
    (this.lift x ⋯).comp
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
        TopCat.carrier) (Spec.map f).base)
⊢ y = this.lift x ⋯
have refine_2₁ : ContinuousMap.comp y
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
      (Spec.map f).base) =
  x
Tactic: rwa [← ContinuousMap.cancel_right (Spec.map f).surjective, Topology.IsQuotientMap.lift_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
S : Scheme
T : Type v
inst : TopologicalSpace T
inst_1 : TotallyDisconnectedSpace T
U : Scheme
f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T
⊢ (fun (f : (continuousMapPresheaf T).obj (Opposite.op U)) ↦
        { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ : ContinuousMap.{u, v} (ConnectedComponents ↥U) T })
      ((fun (f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T) ↦
          f.comp
            { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ :
              C(↥(Opposite.unop (Opposite.op U)), ConnectedComponents ↥U) })
        f) =
    f
have a : Eq (α := (a : ConnectedComponents ↥U) → T)
  (⇑((fun (f : (continuousMapPresheaf T).obj (Opposite.op U)) ↦
          { toFun := sorry.connectedComponentsLift, continuous_toFun := sorry :
            ContinuousMap.{u, v} (ConnectedComponents ↥U) T })
        ((fun (f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T) ↦
            f.comp
              { toFun := ConnectedComponents.mk, continuous_toFun := sorry :
                C(↥(Opposite.unop (Opposite.op U)), ConnectedComponents ↥U) })
          f)) :
    (a : ConnectedComponents ↥U) → T)
  (⇑f : (a : ConnectedComponents ↥U) → T)
Tactic: apply ContinuousMap.coe_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
S : Scheme
T : Type v
inst : TopologicalSpace T
inst_1 : TotallyDisconnectedSpace T
U : Scheme
f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T
⊢ Eq (α := (a : ConnectedComponents ↥U) → T)
    (⇑((fun (f : (continuousMapPresheaf T).obj (Opposite.op U)) ↦
            { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ :
              ContinuousMap.{u, v} (ConnectedComponents ↥U) T })
          ((fun (f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T) ↦
              f.comp
                { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ :
                  C(↥(Opposite.unop (Opposite.op U)), ConnectedComponents ↥U) })
            f)) :
      (a : ConnectedComponents ↥U) → T)
    (⇑f : (a : ConnectedComponents ↥U) → T)
have a : Eq (α := (a : ConnectedComponents ↥U) → T)
  (Continuous.connectedComponentsLift (f :=
    Function.comp (β := ConnectedComponents ↥U) (⇑f : (a : ConnectedComponents ↥U) → T) ConnectedComponents.mk) sorry)
  (⇑f : (a : ConnectedComponents ↥U) → T)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (goal)
Goal:
A : Type v
inst : TopologicalSpace A
inst_1 : AddCommGroup A
inst_2 : IsTopologicalAddGroup A
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheafAb A)
have apply : Presheaf.IsSheaf Scheme.fpqcTopology
  (continuousMapPresheafAb A ⋙
    forget Ab (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 v)) →+ (↑x2 : Type (max u_1 v))) (CC :=
      AddCommGrpCat.carrier))
Tactic: apply Presheaf.isSheaf_of_isSheaf_comp _ _ (forget Ab)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ElladicCohomology (hypothesis)
Goal:
X : Scheme
⊢ IsGrothendieckAbelian.{u + 1, u + 1, u + 2} (Sheaf (ProEt.topology X) Ab)
have this : EssentiallySmall.{u + 1, u, u + 1} X.ProEt
Tactic: have : EssentiallySmall.{u + 1} X.ProEt := inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.ElladicCohomology (goal)
Goal:
X : Scheme
ℓ : ℕ
inst : Fact (Nat.Prime ℓ)
inst_1 : IsEmpty.{u + 1} ↥X
n : ℕ
⊢ Subsingleton.{u + 2} (X.EllAdicCohomology ℓ n)
have h : IsZero ((sheafCompose (ProEt.topology X) AddCommGrpCat.uliftFunctor).obj (X.ellAdicSheaf ℓ))
Tactic: apply Sheaf.subsingleton_H_of_isZero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
Goal:
⊢ zariskiTopology ≤ etaleTopology
have hPQ : IsOpenImmersion ≤ @Etale
Tactic: apply grothendieckTopology_monotone
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
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
⊢ ∃ (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
have 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)
Tactic: obtain ⟨⟨x, a⟩, rfl⟩ := (Scheme.SpecToEquivOfField Ω S).symm.surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
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 Ω
⊢ ∃ (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)
have 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)
Tactic: rw [mem_grothendieckTopology_iff] at hR
Cleared hypotheses: hR, x, a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
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 Ω
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨𝒰, hle⟩ := hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
Cleared hypotheses: x, a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
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)
have 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)
Tactic: refine ⟨𝒰.X i, 𝒰.f i, hle _ _ ⟨i⟩, ?_⟩