awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s :
  (↑((fun (x : (↑X.toTopCat : Type u)) ↦
          Classical.choose (p := fun (R : CommRingCat.{u}) ↦
            Nonempty.{u + 1}
              (X.restrict (U :=
                  Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                            Classical.choose (p := fun (U : OpenNhds x) ↦
                              ∃ (R : CommRingCat.{u}),
                                Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)
                          x) :
                      TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                  (f :=
                  (Opens.inclusion'
                      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                ∃ (R : CommRingCat.{u}),
                                  Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯)
                            x) :
                        TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                    Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                      X.toTopCat))
                  ⋯ ≅
                Spec.toLocallyRingedSpace.obj (op R)))
            ⋯)
        (Cover.idx X.affineCover a)) :
    Type u)
hxV :
  x ∈
    (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u)))
hVU :
  (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
    U'
⊢ Membership.mem (γ := Set ↥X)
    (Set.image (α := ↥(X.affineCover.X (Cover.idx X.affineCover a))) (⇑(X.affineCover.f (Cover.idx X.affineCover a)))
      (Opens.carrier (PrimeSpectrum.basicOpen s)))
    a

Tactic:
exact ⟨x, hxV, e⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s :
  (↑((fun (x : (↑X.toTopCat : Type u)) ↦
          Classical.choose (p := fun (R : CommRingCat.{u}) ↦
            Nonempty.{u + 1}
              (X.restrict (U :=
                  Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                            Classical.choose (p := fun (U : OpenNhds x) ↦
                              ∃ (R : CommRingCat.{u}),
                                Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)
                          x) :
                      TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                  (f :=
                  (Opens.inclusion'
                      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                ∃ (R : CommRingCat.{u}),
                                  Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯)
                            x) :
                        TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                    Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                      X.toTopCat))
                  ⋯ ≅
                Spec.toLocallyRingedSpace.obj (op R)))
            ⋯)
        (Cover.idx X.affineCover a)) :
    Type u)
hxV :
  x ∈
    (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u)))
hVU :
  (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
    U'
h_nhds :
  Subset (α := Set ↥(X.affineCover.X (Cover.idx X.affineCover a))) (Opens.carrier (PrimeSpectrum.basicOpen s))
    (⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U)
⊢ Set.image (α := ↥(X.affineCover.X (Cover.idx X.affineCover a))) (⇑(X.affineCover.f (Cover.idx X.affineCover a)))
      (Opens.carrier (PrimeSpectrum.basicOpen s)) ⊆
    U

Tactic:
rw [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s :
  (↑((fun (x : (↑X.toTopCat : Type u)) ↦
          Classical.choose (p := fun (R : CommRingCat.{u}) ↦
            Nonempty.{u + 1}
              (X.restrict (U :=
                  Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                            Classical.choose (p := fun (U : OpenNhds x) ↦
                              ∃ (R : CommRingCat.{u}),
                                Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)
                          x) :
                      TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                  (f :=
                  (Opens.inclusion'
                      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                ∃ (R : CommRingCat.{u}),
                                  Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯)
                            x) :
                        TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                    Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                      X.toTopCat))
                  ⋯ ≅
                Spec.toLocallyRingedSpace.obj (op R)))
            ⋯)
        (Cover.idx X.affineCover a)) :
    Type u)
hxV :
  x ∈
    (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u)))
hVU :
  (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
    U'
⊢ Subset (α := Set ↥(X.affineCover.X (Cover.idx X.affineCover a))) (Opens.carrier (PrimeSpectrum.basicOpen s))
    (⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U)

Tactic:
hVU

Premises used: Set.Mem
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s :
  (↑((fun (x : (↑X.toTopCat : Type u)) ↦
          Classical.choose (p := fun (R : CommRingCat.{u}) ↦
            Nonempty.{u + 1}
              (X.restrict (U :=
                  Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                            Classical.choose (p := fun (U : OpenNhds x) ↦
                              ∃ (R : CommRingCat.{u}),
                                Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)
                          x) :
                      TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                  (f :=
                  (Opens.inclusion'
                      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                ∃ (R : CommRingCat.{u}),
                                  Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯)
                            x) :
                        TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                    Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                      X.toTopCat))
                  ⋯ ≅
                Spec.toLocallyRingedSpace.obj (op R)))
            ⋯)
        (Cover.idx X.affineCover a)) :
    Type u)
hxV :
  x ∈
    (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u)))
hVU :
  (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
    U'
⊢ Subset (α := Set ↥(X.affineCover.X (Cover.idx X.affineCover a))) (Opens.carrier (PrimeSpectrum.basicOpen s))
    (⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U)

Tactic:
exact hVU
-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
rw :
  (∀ (x : ↥W),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
        Membership.mem (γ := Set ↥W)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                        (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                        (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
      P
        (PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
              (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) } ∈
    (precoverage P).coverings W

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
⊢ (∀ (x : ↥W),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
        Membership.mem (γ := Set ↥W)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                        (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                        (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
      P
        (PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i)

Tactic:
⟨fun x ↦ ?_, fun j ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
x : ↥W
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hy : ∃ (y : ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)), ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) y = x
h :
  Membership.mem (γ := Set ↥W)
    (Set.range (ι :=
      ↥(PreZeroHypercover.X
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
      ⇑(PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
    x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
              (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
    Membership.mem (γ := Set ↥W)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
      x

Tactic:
use i
-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
x : ↥W
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hy : ∃ (y : ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)), ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) y = x
⊢ Membership.mem (γ := Set ↥W)
    (Set.range (ι :=
      ↥(PreZeroHypercover.X
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
      ⇑(PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                  (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
    x

Tactic:
(mem_range_iff_of_surjective ((𝒰.pullback₁ f).f i) _
        ((PreservesPullback.iso (Over.forget S) (f.asOver S) ((𝒰.f _).asOver S)).inv)
        (PreservesPullback.iso_inv_fst _ _ _) x).mp hy

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, Set.Mem, CategoryTheory.Limits.PreservesPullback.iso_inv_fst, CategoryTheory.Limits.PreservesPullback.iso, CategoryTheory.Over.forget, AlgebraicGeometry.mem_range_iff_of_surjective, Iff.mp, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover