awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (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, 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
-- 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
j :
  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)) }
refine_2 :
  P (X :=
    (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X j) S) (Z := OverClass.asOver X S) (Hom.asOver f S)
        (Hom.asOver (𝒰.f j) S)).left)
    (Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f j) 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 }
      j)

Tactic:
dsimp only
-- 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
j :
  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)) }
refine_2 :
  P (X :=
    pullback (X := Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver W S)) (Y :=
      Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver (𝒰.X j) S)) (Z :=
      Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver X S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))
    (pullback.fst (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))
⊢ P (X :=
    (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X j) S) (Z := OverClass.asOver X S) (Hom.asOver f S)
        (Hom.asOver (𝒰.f j) S)).left)
    (Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f j) S)))

Tactic:
rw [← Over.forget_map, ← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Limits.PreservesPullback.iso_hom_fst, CategoryTheory.Over.forget_map, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- 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
j :
  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 (X :=
    pullback (X := Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver W S)) (Y :=
      Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver (𝒰.X j) S)) (Z :=
      Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver X S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))
    (pullback.fst (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))

Tactic:
P.pullback_fst _ _ (𝒰.map_prop j)

Premises used: CategoryTheory.MorphismProperty.pullback_fst, AlgebraicGeometry.Scheme.Cover.map_prop
-- 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
j :
  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 (X :=
    pullback (X := Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver W S)) (Y :=
      Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver (𝒰.X j) S)) (Z :=
      Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver X S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))
    (pullback.fst (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
      (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))

Tactic:
exact P.pullback_fst _ _ (𝒰.map_prop j)

Premises used: CategoryTheory.MorphismProperty.pullback_fst, AlgebraicGeometry.Scheme.Cover.map_prop
-- 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
j : (Cover.pullbackCoverOver (P := P) S 𝒰 f).I₀
⊢ (Cover.pullbackCoverOver (P := P) S 𝒰 f).f j ≫ W ↘ S = (Cover.pullbackCoverOver (P := P) S 𝒰 f).X j ↘ S

Tactic:
Over.w (pullback.fst (f.asOver S) ((𝒰.f j).asOver S))

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, CategoryTheory.over, CategoryTheory.Over.w, CategoryTheory.Limits.pullback.fst, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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
j : (Cover.pullbackCoverOver (P := P) S 𝒰 f).I₀
⊢ (Cover.pullbackCoverOver (P := P) S 𝒰 f).f j ≫ W ↘ S = (Cover.pullbackCoverOver (P := P) S 𝒰 f).X j ↘ S

Tactic:
exact Over.w (pullback.fst (f.asOver S) ((𝒰.f j).asOver S))

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Over.w, CategoryTheory.Limits.pullback.fst, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
        Membership.mem (γ := Set ↥W)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                        (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                        (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
      P
        (PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
              (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
        Membership.mem (γ := Set ↥W)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                        (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                        (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
                  f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
      P
        (PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
      ⇑(PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
              (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
    Membership.mem (γ := Set ↥W)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                    (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                    (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
      ⇑(PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
    x

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

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, Set.Mem, CategoryTheory.Limits.PreservesPullback.iso_inv_snd, CategoryTheory.Precoverage.ZeroHypercover.pullback₂, CategoryTheory.Limits.PreservesPullback.iso, CategoryTheory.Over.forget, AlgebraicGeometry.mem_range_iff_of_surjective, Iff.mp, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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 (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
      ⇑(PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                  (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
            f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
    x

Tactic:
exact (mem_range_iff_of_surjective ((𝒰.pullback₂ f).f _) _
        ((PreservesPullback.iso (Over.forget S) ((𝒰.f _).asOver S) (f.asOver S)).inv)
        (PreservesPullback.iso_inv_snd _ _ _) x).mp hy

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.PreservesPullback.iso_inv_snd, CategoryTheory.Precoverage.ZeroHypercover.pullback₂, CategoryTheory.Limits.PreservesPullback.iso, CategoryTheory.Over.forget, AlgebraicGeometry.mem_range_iff_of_surjective, Iff.mp, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
            (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
      f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }
refine_2 :
  P (X :=
    (pullback (X := OverClass.asOver (𝒰.X j) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
        (Hom.asOver (𝒰.f j) S) (Hom.asOver f S)).left)
    (Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f j) S) (Hom.asOver f S)))
⊢ P
    (PreZeroHypercover.f
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
              (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
        PreZeroHypercover.{u_1, u, u + 1} W }
      j)

Tactic:
dsimp only