awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
inst_1 : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve.{v, u} X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (E.weaken ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (E.weaken ⋯) : ZeroHypercover.Small.Index (E.weaken ⋯) → (E.weaken ⋯).I₀)) ≤
    E.presieve₀

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
inst_1 : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve.{v, u} X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (E.weaken ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (E.weaken ⋯) : ZeroHypercover.Small.Index (E.weaken ⋯) → (E.weaken ⋯).I₀)) ∈
    K.coverings S

Tactic:
exact of_le (by simp) E.mem₀.2

Premises used: And.right, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
J.mem_coverings_of_isPullback (fun i ↦ E.f (e.inv.s₀ i)) ?_ (𝟙 S) _ (fun i ↦ ?_) ?_

Premises used: CategoryTheory.PreZeroHypercover.f, Set.Mem, CategoryTheory.CategoryStruct.id, CategoryTheory.Precoverage.mem_coverings_of_isPullback, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
refine_1 : (Presieve.ofArrows (fun (i : F.I₀) ↦ E.X (e.inv.s₀ i)) fun (i : F.I₀) ↦ E.f (e.inv.s₀ i)) ∈ J.coverings S
refine_2 : (i : F.I₀) → F.X i ⟶ E.X (e.inv.s₀ i)
refine_3 :
  ∀ (i : F.I₀),
    IsPullback (Y := E.X (e.inv.s₀ i)) (F.f i) ((fun (i : F.I₀) ↦ e.inv.h₀ i) i) (𝟙 S)
      ((fun (i : F.I₀) ↦ (E.f (e.inv.s₀ i) : E.X (e.inv.s₀ i) ⟶ S)) i)
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
refine J.mem_coverings_of_isPullback (fun i ↦ E.f (e.inv.s₀ i)) ?_ (𝟙 S) _ (fun i ↦ ?_) ?_

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.CategoryStruct.id, CategoryTheory.Precoverage.mem_coverings_of_isPullback, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ E.presieve₀ ∈ J.coverings S

Tactic:
h
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
h₁ : (Presieve.ofArrows (fun (i : F.I₀) ↦ E.X (e.inv.s₀ i)) fun (i : F.I₀) ↦ E.f (e.inv.s₀ i)) = E.presieve₀
⊢ (Presieve.ofArrows (fun (i : F.I₀) ↦ E.X (e.inv.s₀ i)) fun (i : F.I₀) ↦ E.f (e.inv.s₀ i)) ∈ J.coverings S

Tactic:
convert! h
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : E.I₀
⊢ e.inv.s₀ (e.hom.s₀ i) = i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ (Presieve.ofArrows (fun (i : F.I₀) ↦ E.X (e.inv.s₀ i)) fun (i : F.I₀) ↦ E.f (e.inv.s₀ i)) = E.presieve₀

Tactic:
exact Presieve.ofArrows_comp_eq_of_surjective _ (fun i ↦ ⟨e.hom.s₀ i, by simp⟩)

Premises used: CategoryTheory.Presieve.ofArrows_comp_eq_of_surjective, Exists.intro, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ F.X i ⟶ E.X (e.inv.s₀ i)

Tactic:
exact e.inv.h₀ i

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ CommSq (Y := E.X (e.inv.s₀ i)) (F.f i) ((fun (i : F.I₀) ↦ e.inv.h₀ i) i) (𝟙 S)
    ((fun (i : F.I₀) ↦ (E.f (e.inv.s₀ i) : E.X (e.inv.s₀ i) ⟶ S)) i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ IsPullback (Y := E.X (e.inv.s₀ i)) (F.f i) ((fun (i : F.I₀) ↦ e.inv.h₀ i) i) (𝟙 S)
    ((fun (i : F.I₀) ↦ (E.f (e.inv.s₀ i) : E.X (e.inv.s₀ i) ⟶ S)) i)

Tactic:
exact CategoryTheory.IsPullback.of_vert_isIso (by simp)

Premises used: CategoryTheory.IsPullback.of_vert_isIso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
X : C
R : Presieve.{v, u} X
⊢ R ∈ P.precoverage.coverings X ↔ ∃ (E : PreZeroHypercover X), P.property E ∧ R = E.presieve₀

Tactic:
⟨fun ⟨E, hE⟩ ↦ ⟨E, hE, rfl⟩, fun ⟨_, hE, h⟩ ↦ h ▸ ⟨_, hE⟩⟩

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, CategoryTheory.PreZeroHypercoverFamily.precoverage, _private.0.CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff.match_1, Membership.mem, Exists, CategoryTheory.PreZeroHypercoverFamily.presieve.mk, Eq.rec, _private.0.CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff.match_2, And, And.intro, Iff.intro, CategoryTheory.PreZeroHypercoverFamily.property, Exists.intro, CategoryTheory.Precoverage.coverings, Eq.symm, Eq, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
X : C
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E

Tactic:
⟨fun h ↦ ?_, fun h ↦ .mk _ h⟩

Premises used: CategoryTheory.PreZeroHypercoverFamily.presieve.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
X : C
E : PreZeroHypercover X
refine : ∀ (h : E.presieve₀ ∈ P.precoverage.coverings X), P.property E
⊢ E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ .mk _ h⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
X : C
E : PreZeroHypercover X
h : E.presieve₀ ∈ P.precoverage.coverings X
⊢ ∃ (E_1 : PreZeroHypercover X), P.property E_1 ∧ E.presieve₀ = E_1.presieve₀

Tactic:
rw [PreZeroHypercoverFamily.mem_precoverage_iff] at h

Premises used: CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
X : C
E : PreZeroHypercover X
h : ∃ (E_1 : PreZeroHypercover X), P.property E_1 ∧ E.presieve₀ = E_1.presieve₀
obtain : ∀ (F : PreZeroHypercover X) (h : P.property F) (heq : E.presieve₀ = F.presieve₀), P.property E
⊢ P.property E

Tactic:
obtain ⟨F, h, heq⟩ := h
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
X : C
E F : PreZeroHypercover X
h : P.property F
heq : E.presieve₀ = F.presieve₀
rw : ∀ (h : P.property F.shrink) (heq : E.presieve₀ = F.presieve₀), P.property E.shrink
⊢ P.property E

Tactic:
rw [P.iff_shrink] at h ⊢

Premises used: CategoryTheory.PreZeroHypercoverFamily.iff_shrink
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
rwa rwa₁ rwa₂ rwa₃ : P.property F.shrink
⊢ P.property E.shrink

Tactic:
rwa [PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀ heq]

Premises used: CategoryTheory.PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
X : C
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ K.coverings X ↔ E.shrink.presieve₀ ∈ K.coverings X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
coverings :
  ∀ (X : C) (R : Presieve.{v, u} X),
    Membership.mem (γ := Set (Presieve.{v, u} X))
        (Precoverage.coverings
          ((fun (P : PreZeroHypercoverFamily.{v, u} C) ↦ P.precoverage)
            ((fun (K : Precoverage.{v, u} C) ↦ K.preZeroHypercoverFamily) K))
          X)
        R ↔
      R ∈ K.coverings X
⊢ (fun (P : PreZeroHypercoverFamily.{v, u} C) ↦ P.precoverage)
      ((fun (K : Precoverage.{v, u} C) ↦ K.preZeroHypercoverFamily) K) =
    K

Tactic:
ext X R
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
X : C
R : Presieve.{v, u} X
coverings :
  ∀ (E : PreZeroHypercover X),
    Membership.mem (γ := Set (Presieve.{v, u} X))
        (Precoverage.coverings
          ((fun (P : PreZeroHypercoverFamily.{v, u} C) ↦ P.precoverage)
            ((fun (K : Precoverage.{v, u} C) ↦ K.preZeroHypercoverFamily) K))
          X)
        E.presieve₀ ↔
      E.presieve₀ ∈ K.coverings X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
      (Precoverage.coverings
        ((fun (P : PreZeroHypercoverFamily.{v, u} C) ↦ P.precoverage)
          ((fun (K : Precoverage.{v, u} C) ↦ K.preZeroHypercoverFamily) K))
        X)
      R ↔
    R ∈ K.coverings X

Tactic:
obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover

Premises used: CategoryTheory.Presieve.exists_eq_preZeroHypercover, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
X : C
E : PreZeroHypercover X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
      (coverings
        ((fun (P : PreZeroHypercoverFamily.{v, u} C) ↦ P.precoverage)
          ((fun (K : Precoverage.{v, u} C) ↦ K.preZeroHypercoverFamily) K))
        X)
      E.presieve₀ ↔
    E.presieve₀ ∈ K.coverings X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [IsIso f], P.property (PreZeroHypercover.singleton f)
S T : C
f : S ⟶ T
hf : IsIso f
rw : (PreZeroHypercover.singleton f).presieve₀ ∈ P.precoverage.coverings T
⊢ Presieve.singleton f ∈ P.precoverage.coverings T

Tactic:
rw [← PreZeroHypercover.presieve₀_singleton.{_, _, max u v}]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [IsIso f], P.property (PreZeroHypercover.singleton f)
S T : C
f : S ⟶ T
hf : IsIso f
⊢ (PreZeroHypercover.singleton f).presieve₀ ∈ P.precoverage.coverings T

Tactic:
.mk _ (h _)

Premises used: Set.Mem, setOf, CategoryTheory.PreZeroHypercoverFamily.presieve.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [IsIso f], P.property (PreZeroHypercover.singleton f)
S T : C
f : S ⟶ T
hf : IsIso f
⊢ (PreZeroHypercover.singleton f).presieve₀ ∈ P.precoverage.coverings T

Tactic:
refine .mk _ (h _)
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h₁ : ∀ {X : C}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) P.property
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
⊢ ∀ (i : E.I₀), HasPullback g (E.f i)

Tactic:
have (i : E.I₀) : HasPullback g (E.f i) := (h i).hasPullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h₁ : ∀ {X : C}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) P.property
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
e : F ≅ PreZeroHypercover.pullback₁ g E := PreZeroHypercover.isoMk (Equiv.refl F.I₀) (fun (i : F.I₀) ↦ ⋯.isoPullback) ⋯
change : F.presieve₀ ∈ P.precoverage.coverings Y
⊢ Presieve.ofArrows Z p₁ ∈ P.precoverage.coverings Y

Tactic:
change F.presieve₀ ∈ _

Premises used: CategoryTheory.PreZeroHypercover.presieve₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h₁ : ∀ {X : C}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) P.property
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
e : F ≅ PreZeroHypercover.pullback₁ g E := PreZeroHypercover.isoMk (Equiv.refl F.I₀) (fun (i : F.I₀) ↦ ⋯.isoPullback) ⋯
rw : P.property (PreZeroHypercover.pullback₁ g E)
⊢ F.presieve₀ ∈ P.precoverage.coverings Y

Tactic:
rw [F.presieve₀_mem_precoverage_iff, (P (X := Y)).prop_iff_of_iso e]

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.PreZeroHypercoverFamily.property, CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h₁ : ∀ {X : C}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) P.property
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
e : F ≅ PreZeroHypercover.pullback₁ g E := PreZeroHypercover.isoMk (Equiv.refl F.I₀) (fun (i : F.I₀) ↦ ⋯.isoPullback) ⋯
⊢ P.property (PreZeroHypercover.pullback₁ g E)

Tactic:
h₂ _ _ ?_
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h₁ : ∀ {X : C}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) P.property
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
e : F ≅ PreZeroHypercover.pullback₁ g E := PreZeroHypercover.isoMk (Equiv.refl F.I₀) (fun (i : F.I₀) ↦ ⋯.isoPullback) ⋯
refine : P.property E
⊢ P.property (PreZeroHypercover.pullback₁ g E)

Tactic:
refine h₂ _ _ ?_
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h₁ : ∀ {X : C}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) P.property
h₂ :
  ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)],
    P.property E → P.property (PreZeroHypercover.pullback₁ f E)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
Y : C
g : Y ⟶ S
Z : ι → C
p₁ : (i : ι) → Z i ⟶ Y
p₂ : (i : ι) → Z i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : ∀ (i : E.I₀), HasPullback g (E.f i)
F : PreZeroHypercover Y := { I₀ := ι, X := Z, f := p₁ }
e : F ≅ PreZeroHypercover.pullback₁ g E := PreZeroHypercover.isoMk (Equiv.refl F.I₀) (fun (i : F.I₀) ↦ ⋯.isoPullback) ⋯
rwa rwa₁ rwa₂ rwa₃ : E.presieve₀ ∈ P.precoverage.coverings S
⊢ P.property E

Tactic:
rwa [← E.presieve₀_mem_precoverage_iff]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (X i))) (P.precoverage.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun (i : ι) ↦ { I₀ := σ i, X := Y i, f := g i }
⊢ (Presieve.ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (x : (i : ι) × σ i) ↦
      g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i))) ∈
    P.precoverage.coverings S

Tactic:
(E.bind F).presieve₀_mem_precoverage_iff.mpr (h _ _ ?_ fun i ↦ ?_)

Premises used: Iff.mpr, Set.Mem, setOf, CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (X i))) (P.precoverage.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun (i : ι) ↦ { I₀ := σ i, X := Y i, f := g i }
refine_1 : P.property E
refine_2 : ∀ (i : E.I₀), P.property (F i)
⊢ (Presieve.ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (x : (i : ι) × σ i) ↦
      g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i))) ∈
    P.precoverage.coverings S

Tactic:
refine (E.bind F).presieve₀_mem_precoverage_iff.mpr (h _ _ ?_ fun i ↦ ?_)

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (X i))) (P.precoverage.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun (i : ι) ↦ { I₀ := σ i, X := Y i, f := g i }
refine_1 refine_1₁ refine_1₂ refine_1₃ : E.presieve₀ ∈ P.precoverage.coverings S
⊢ P.property E

Tactic:
rwa [← E.presieve₀_mem_precoverage_iff]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (X i))) (P.precoverage.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun (i : ι) ↦ { I₀ := σ i, X := Y i, f := g i }
i : E.I₀
refine_2 : Membership.mem (γ := Set (Presieve.{v, u} (E.X i))) (P.precoverage.coverings (E.X i)) (F i).presieve₀
⊢ P.property (F i)

Tactic:
rw [← (F i).presieve₀_mem_precoverage_iff]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (X i))) (P.precoverage.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun (i : ι) ↦ { I₀ := σ i, X := Y i, f := g i }
i : E.I₀
⊢ Membership.mem (γ := Set (Presieve.{v, u} (E.X i))) (P.precoverage.coverings (E.X i)) (F i).presieve₀

Tactic:
hg i

Premises used: Set.Mem, setOf