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
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ 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₀) ↦
              (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
                    X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S)
                    (Hom.asOverProp (P := Q) f S))).left,
            f := fun (x : 𝒰.I₀) ↦
              CommaMorphism.left
                (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
      ⇑(PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
                    X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S)
                    (Hom.asOverProp (P := Q) f S))).left,
            f := fun (x : 𝒰.I₀) ↦
              CommaMorphism.left
                (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
    x

Tactic:
(mem_range_iff_of_surjective ((𝒰.pullback₂ f).f i) _
        ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
          ((𝒰.f _).asOverProp S) (f.asOverProp S)).inv)
        (PreservesPullback.iso_inv_snd _ _ _) x).mp hy

Premises used: CategoryTheory.PreZeroHypercover.f, Set.Mem, AlgebraicGeometry.Scheme.Hom.asOverProp, CategoryTheory.Functor.comp, 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.MorphismProperty.Over.forget, 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
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ 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₀) ↦
              (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
                    X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S)
                    (Hom.asOverProp (P := Q) f S))).left,
            f := fun (x : 𝒰.I₀) ↦
              CommaMorphism.left
                (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
      ⇑(PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
                    X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S)
                    (Hom.asOverProp (P := Q) f S))).left,
            f := fun (x : 𝒰.I₀) ↦
              CommaMorphism.left
                (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i))
    x

Tactic:
exact (mem_range_iff_of_surjective ((𝒰.pullback₂ f).f i) _
        ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
          ((𝒰.f _).asOverProp S) (f.asOverProp S)).inv)
        (PreservesPullback.iso_inv_snd _ _ _) x).mp hy

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.asOverProp, CategoryTheory.Functor.comp, 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.MorphismProperty.Over.forget, 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
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) }
refine_2 :
  P (X :=
    (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
        (pullback (X := (𝒰.X j).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))).left)
    (Y := W)
    (CategoryTheory.Functor.map (Over.forget S)
        (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
          (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))) :
      Functor.obj (Over.forget S)
          (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := (𝒰.X j).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f j) S) (Hom.asOverProp (P := Q) f S))) ⟶
        Functor.obj (Over.forget S) (W.asOver S))
⊢ P
    (PreZeroHypercover.f
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
              (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
                X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))).left,
        f := fun (x : 𝒰.I₀) ↦
          CommaMorphism.left
            (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
              (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) :
        PreZeroHypercover.{u_1, u, u + 1} W }
      j)

Tactic:
simp only [← CategoryTheory.Over.forget_map]

Premises used: CategoryTheory.Over.forget_map
-- 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
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) }
⊢ P (X :=
    pullback (X :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        ((𝒰.X j).asOverProp (P := Q) S ⋯))
      (Y :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (W.asOverProp (P := Q) S hW))
      (Z :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (X.asOverProp (P := Q) S hX))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) (𝒰.f j) S))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) f S)))
    (pullback.snd
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) (𝒰.f j) S))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) f S)))

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

Premises used: CategoryTheory.MorphismProperty.pullback_snd, 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
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := (𝒰.X x).asOverProp (P := Q) S ⋯) (Y := W.asOverProp (P := Q) S hW) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.snd (Hom.asOverProp (P := Q) (𝒰.f x) S) (Hom.asOverProp (P := Q) f S))) }
⊢ P (X :=
    pullback (X :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        ((𝒰.X j).asOverProp (P := Q) S ⋯))
      (Y :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (W.asOverProp (P := Q) S hW))
      (Z :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (X.asOverProp (P := Q) S hX))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) (𝒰.f j) S))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) f S)))
    (pullback.snd
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) (𝒰.f j) S))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) f S)))

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

Premises used: CategoryTheory.MorphismProperty.pullback_snd, 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
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j : (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f (Q := Q) hX hW hQ).I₀
⊢ (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f (Q := Q) hX hW hQ).f j ≫ W ↘ S =
    (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f (Q := Q) hX hW hQ).X j ↘ S

Tactic:
(pullback.snd ((𝒰.f j).asOverProp S) (f.asOverProp S)).w

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.PreZeroHypercover.f, Set.Mem, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Hom.asOverProp, setOf, ContinuousMap.comp, CategoryTheory.CommaMorphism.w, CategoryTheory.over, Set.preimage, AlgebraicGeometry.PresheafedSpace.comp, AlgebraicGeometry.LocallyRingedSpace.comp, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism, 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
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j : (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f (Q := Q) hX hW hQ).I₀
⊢ (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f (Q := Q) hX hW hQ).f j ≫ W ↘ S =
    (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f (Q := Q) hX hW hQ).X j ↘ S

Tactic:
exact (pullback.snd ((𝒰.f j).asOverProp S) (f.asOverProp S)).w

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Hom.asOverProp, CategoryTheory.CommaMorphism.w, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
inst_2 : P.IsStableUnderComposition
X_1 : Scheme
𝒰_1 : Cover (precoverage P) X_1
𝒱_1 : (x : 𝒰_1.I₀) → Cover.{?u.103208, u} (precoverage P) (𝒰_1.X x)
inst_3 : X_1.Over S
inst_4 : Cover.Over S (P := P) 𝒰_1
inst_5 : (x : 𝒰_1.I₀) → Cover.Over S (P := P) (𝒱_1 x)
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
𝒱 : (x : 𝒰.I₀) → Cover.{u_2, u} (precoverage P) (𝒰.X x)
inst_6 : X.Over S
inst_7 : Cover.Over S (P := P) 𝒰
inst_8 : (x : 𝒰.I₀) → Cover.Over S (P := P) (𝒱 x)
x : (Precoverage.ZeroHypercover.bind 𝒰 𝒱).I₀
i : 𝒰.I₀
j : PreZeroHypercover.I₀.{u_2, u, u + 1} (C := Scheme) (S := 𝒰.X i) ((fun (i : 𝒰.I₀) ↦ (𝒱 i).toPreZeroHypercover) i)
simp : (𝒱 i).X j ↘ S = (𝒱 i).X j ↘ S
⊢ (Precoverage.ZeroHypercover.bind 𝒰 𝒱).f
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀.{u_2, u, u + 1} (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦ (𝒱 i).toPreZeroHypercover) i))
          i j) ≫
      X ↘ S =
    (Precoverage.ZeroHypercover.bind 𝒰 𝒱).X
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀.{u_2, u, u + 1} (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦ (𝒱 i).toPreZeroHypercover) i))
          i j) ↘
      S

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
inst_2 : P.IsStableUnderComposition
X_1 : Scheme
𝒰_1 : Cover (precoverage P) X_1
𝒱_1 : (x : 𝒰_1.I₀) → Cover.{?u.103208, u} (precoverage P) (𝒰_1.X x)
inst_3 : X_1.Over S
inst_4 : Cover.Over S (P := P) 𝒰_1
inst_5 : (x : 𝒰_1.I₀) → Cover.Over S (P := P) (𝒱_1 x)
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
𝒱 : (x : 𝒰.I₀) → Cover.{u_2, u} (precoverage P) (𝒰.X x)
inst_6 : X.Over S
inst_7 : Cover.Over S (P := P) 𝒰
inst_8 : (x : 𝒰.I₀) → Cover.Over S (P := P) (𝒱 x)
x : (Precoverage.ZeroHypercover.bind 𝒰 𝒱).I₀
i : 𝒰.I₀
j : PreZeroHypercover.I₀.{u_2, u, u + 1} (C := Scheme) (S := 𝒰.X i) ((fun (i : 𝒰.I₀) ↦ (𝒱 i).toPreZeroHypercover) i)
⊢ (𝒱 i).X j ↘ S = (𝒱 i).X j ↘ S

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)

Tactic:
QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen hU

Premises used: AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
obtain :
  ∀ (Us : Set (TopologicalSpace.Opens ↥S)) (hUs : Us ⊆ S.affineOpens) (hUf : Us.Finite) (hUc : U = sSup Us),
    IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)

Tactic:
obtain ⟨Us, hUs, hUf, hUc⟩ := S.isBasis_affineOpens.exists_finite_of_isCompact hU

Premises used: TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
Us : Set (TopologicalSpace.Opens ↥S)
hUs : Us ⊆ S.affineOpens
hUf : Us.Finite
hUc : U = sSup Us
⊢ ⋃ t ∈ SetLike.coe '' Us, t = (↑U : Set ↥S)

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
Us : Set (TopologicalSpace.Opens ↥S)
hUs : Us ⊆ S.affineOpens
hUf : Us.Finite
hUc : U = sSup Us
refine : ∀ t ∈ SetLike.coe '' Us, IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) t
⊢ IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) (↑U : Set ↥S)

Tactic:
refine .of_biUnion_eq_of_finite (SetLike.coe '' Us) (by simp_all) (hUf.image _) ?_
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
Us : Set (TopologicalSpace.Opens ↥S)
hUs : Us ⊆ S.affineOpens
hUf : Us.Finite
hUc : U = sSup Us
⊢ ∀ t ∈ SetLike.coe '' Us, IsCompactOpenCovered (X := fun (x : 𝒰.I₀) ↦ ↥(𝒰.X x)) (fun (x : 𝒰.I₀) ↦ ⇑(𝒰.f x)) t

Tactic:
simpa using fun t ht ↦ IsAffineOpen.isCompactOpenCovered 𝒰 (hUs ht)

Premises used: AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
obtain :
  ∀ (n : ℕ) (a : Fin n → 𝒰.I₀) (V : (i : Fin n) → TopologicalSpace.Opens ↥(𝒰.X (a i)))
    (ha : ∀ (i : Fin n), Membership.mem (γ := Set (TopologicalSpace.Opens ↥(𝒰.X (a i)))) (𝒰.X (a i)).affineOpens (V i))
    (heq : ⋃ (i : Fin n), ⇑(𝒰.f (a i)) '' (↑(V i) : Set ↥(𝒰.X (a i))) = (↑U : Set ↥S)),
    ∃ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens),
      (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑U : Set ↥S)
⊢ ∃ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens),
    (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑U : Set ↥S)

Tactic:
obtain ⟨n, a, V, ha, heq⟩ := (isCompactOpenCovered_of_isCompact 𝒰 hU).exists_mem_of_isBasis
    (fun i ↦ (𝒰.X i).isBasis_affineOpens) (fun _ _ h ↦ h.isCompact)

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, IsCompactOpenCovered.exists_mem_of_isBasis, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
n : ℕ
a : Fin n → 𝒰.I₀
V : (i : Fin n) → TopologicalSpace.Opens ↥(𝒰.X (a i))
ha : ∀ (i : Fin n), Membership.mem (γ := Set (TopologicalSpace.Opens ↥(𝒰.X (a i)))) (𝒰.X (a i)).affineOpens (V i)
heq : ⋃ (i : Fin n), ⇑(𝒰.f (a i)) '' (↑(V i) : Set ↥(𝒰.X (a i))) = (↑U : Set ↥S)
⊢ ∃ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens),
    (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑U : Set ↥S)

Tactic:
⟨n, a, V, ha, heq⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
inst : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact (↑U : Set ↥S)
n : ℕ
a : Fin n → 𝒰.I₀
V : (i : Fin n) → TopologicalSpace.Opens ↥(𝒰.X (a i))
ha : ∀ (i : Fin n), Membership.mem (γ := Set (TopologicalSpace.Opens ↥(𝒰.X (a i)))) (𝒰.X (a i)).affineOpens (V i)
heq : ⋃ (i : Fin n), ⇑(𝒰.f (a i)) '' (↑(V i) : Set ↥(𝒰.X (a i))) = (↑U : Set ↥S)
⊢ ∃ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens),
    (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ (i : Fin n), ⇑(𝒰.f (f i)) '' (↑(V i) : Set ↥(𝒰.X (f i))) = (↑U : Set ↥S)

Tactic:
exact ⟨n, a, V, ha, heq⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰_1 𝒰_2 : PreZeroHypercover.{v, u, u + 1} S
K : Precoverage Scheme
𝒰 : Scheme.OpenCover.{u_1, u} S
⊢ QuasiCompactCover 𝒰.toPreZeroHypercover

Tactic:
of_isOpenMap fun i ↦ (𝒰.f i).isOpenEmbedding.isOpenMap

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.QuasiCompactCover.of_isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Goal:
S : Scheme
𝒰 : PreZeroHypercover.{v, u, u + 1} S
𝒱 : PreZeroHypercover.{w', u, u + 1} S
f : 𝒱.Hom 𝒰
inst : QuasiCompactCover 𝒱
⊢ QuasiCompactCover 𝒰

Tactic:
⟨fun {U} hU ↦ ?_⟩

Premises used: AlgebraicGeometry.QuasiCompactCover.mk