awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
R : Presieve.{v, u} X
hR : R ∈ J.coverings X
⊢ ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
have obtain : ∀ (ι : Type (max u v)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X) (hR : Presieve.ofArrows Y f ∈ J.coverings X),
  ∃ (𝒰 : J.ZeroHypercover X), Presieve.ofArrows Y f = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hR : Presieve.ofArrows Y f ∈ J.coverings X
⊢ ∃ (𝒰 : J.ZeroHypercover X), Presieve.ofArrows Y f = Presieve.ofArrows 𝒰.X 𝒰.f
have w : J.ZeroHypercover X
Tactic: use ⟨⟨ι, Y, f⟩, hR⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
X : C
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hR : Presieve.ofArrows Y f ∈ J.coverings X
w : J.ZeroHypercover X
⊢ ∃ (𝒰 : J.ZeroHypercover X), Presieve.ofArrows Y f = Presieve.ofArrows 𝒰.X 𝒰.f
have h : Presieve.ofArrows Y f =
  Presieve.ofArrows { I₀ := ι, X := Y, f := f, mem₀ := hR : J.ZeroHypercover X }.X
    { I₀ := ι, X := Y, f := f, mem₀ := hR : J.ZeroHypercover X }.f
Tactic: use ⟨⟨ι, Y, f⟩, hR⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J K : Precoverage.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
R : Presieve.{v, u} X
hR : R ∈ J.coverings X
⊢ R ∈ K.coverings X
have obtain : ∀ (E : PreZeroHypercover X) (hR : E.presieve₀ ∈ J.coverings X), E.presieve₀ ∈ K.coverings X
Tactic: obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : Precoverage.{v, u} C
inst_1 : J.Small
S : C
E : ZeroHypercover.{w', v, u} J S
⊢ E.Small
have this : E.restrictIndexOfSmall.Small
Tactic: have : ZeroHypercover.Small.{w} (ZeroHypercover.restrictIndexOfSmall.{max u v} E) :=
    Small.zeroHypercoverSmall _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 J : Precoverage.{v, u} C
inst_1 : J.Small
S : C
E : ZeroHypercover.{w', v, u} J S
this : E.restrictIndexOfSmall.Small
E' : ZeroHypercover.{w, v, u} J S := E.restrictIndexOfSmall.restrictIndexOfSmall
⊢ E.Small
have h : PreZeroHypercover.presieve₀.{w, v, u}
    (E.restrictIndex (ι := E'.I₀)
      (Function.comp (β := ZeroHypercover.Small.Index E) (ZeroHypercover.Small.restrictFun E)
          (ZeroHypercover.Small.restrictFun E.restrictIndexOfSmall) :
        E'.I₀ → E.I₀)) ∈
  J.coverings S
Tactic: use E'.I₀, ZeroHypercover.Small.restrictFun _ ∘ ZeroHypercover.Small.restrictFun _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Precoverage.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J : Precoverage.{v_1, u_1} D
inst_2 : J.Small
X : C
E : (comap F J).ZeroHypercover X
⊢ E.Small
have refine : PreZeroHypercover.presieve₀.{w, v, u}
    (E.restrictIndex (ι := (ZeroHypercover.map F E sorry).restrictIndexOfSmall.I₀)
      (ZeroHypercover.Small.restrictFun (ZeroHypercover.map F E sorry) :
        ZeroHypercover.Small.Index (ZeroHypercover.map F E sorry) → (ZeroHypercover.map F E sorry).I₀)) ∈
  (comap F J).coverings X
Tactic: refine ⟨(E.map F le_rfl).restrictIndexOfSmall.I₀, ZeroHypercover.Small.restrictFun _, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
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
⊢ E.Small
have refine_1 : PreZeroHypercover.presieve₀.{w, v, u}
    (E.restrictIndex (ι := (E.weaken sorry).restrictIndexOfSmall.I₀)
      (ZeroHypercover.Small.restrictFun (E.weaken sorry) : ZeroHypercover.Small.Index (E.weaken sorry) → (E.weaken sorry).I₀)) ∈
  J.coverings S
Tactic: refine ⟨(E.weaken (inf_le_left)).restrictIndexOfSmall.I₀,
        ZeroHypercover.Small.restrictFun _, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
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
refine_1 :
  PreZeroHypercover.presieve₀.{w, v, u}
      (E.restrictIndex (ι := (E.weaken ⋯).restrictIndexOfSmall.I₀)
        (ZeroHypercover.Small.restrictFun (E.weaken ⋯) : ZeroHypercover.Small.Index (E.weaken ⋯) → (E.weaken ⋯).I₀)) ∈
    J.coverings S
⊢ E.Small
have refine_2 : PreZeroHypercover.presieve₀.{w, v, u}
    (E.restrictIndex (ι := (E.weaken sorry).restrictIndexOfSmall.I₀)
      (ZeroHypercover.Small.restrictFun (E.weaken sorry) : ZeroHypercover.Small.Index (E.weaken sorry) → (E.weaken sorry).I₀)) ∈
  K.coverings S
Tactic: refine ⟨(E.weaken (inf_le_left)).restrictIndexOfSmall.I₀,
        ZeroHypercover.Small.restrictFun _, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
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
have 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
Tactic: refine J.mem_coverings_of_isPullback (fun i ↦ E.f (e.inv.s₀ i)) ?_ (𝟙 S) _ (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
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
⊢ F.presieve₀ ∈ J.coverings S
have refine_2 : (i : F.I₀) → F.X i ⟶ E.X (e.inv.s₀ i)
Tactic: refine J.mem_coverings_of_isPullback (fun i ↦ E.f (e.inv.s₀ i)) ?_ (𝟙 S) _ (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
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)
⊢ F.presieve₀ ∈ J.coverings S
have 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)
Tactic: refine J.mem_coverings_of_isPullback (fun i ↦ E.f (e.inv.s₀ i)) ?_ (𝟙 S) _ (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
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)) ∈ J.coverings S
have 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₀
Tactic: convert! h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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
have refine : ∀ (h : E.presieve₀ ∈ P.precoverage.coverings X), P.property E
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ .mk _ h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (hypothesis)
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
⊢ P.property E
have h₁ : ∃ (E_1 : PreZeroHypercover X), P.property E_1 ∧ E.presieve₀ = E_1.presieve₀
Tactic: rw [PreZeroHypercoverFamily.mem_precoverage_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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₀
⊢ P.property E
have obtain : ∀ (F : PreZeroHypercover X) (h : P.property F) (heq : E.presieve₀ = F.presieve₀), P.property E
Tactic: obtain ⟨F, h, heq⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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₀
⊢ P.property E
have rw : ∀ (h : P.property F.shrink) (heq : E.presieve₀ = F.presieve₀), P.property E.shrink
Tactic: rw [P.iff_shrink] at h ⊢
Cleared hypotheses: h, heq
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
⊢ (fun (P : PreZeroHypercoverFamily.{v, u} C) ↦ P.precoverage)
      ((fun (K : Precoverage.{v, u} C) ↦ K.preZeroHypercoverFamily) K) =
    K
have coverings : ∀ (X : C) (R : Presieve.{v, u} 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)
      R ↔
    R ∈ K.coverings X
Tactic: ext X R
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
X : C
R : Presieve.{v, u} 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)
      R ↔
    R ∈ K.coverings X
have coverings : ∀ (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: obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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
⊢ Presieve.singleton f ∈ P.precoverage.coverings T
have rw : (PreZeroHypercover.singleton f).presieve₀ ∈ P.precoverage.coverings T
Tactic: rw [← PreZeroHypercover.presieve₀_singleton.{_, _, max u v}]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (hypothesis)
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 }
⊢ Presieve.ofArrows Z p₁ ∈ P.precoverage.coverings Y
have this : ∀ (i : E.I₀), HasPullback g (E.f i)
Tactic: have (i : E.I₀) : HasPullback g (E.f i) := (h i).hasPullback
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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) ⋯
⊢ Presieve.ofArrows Z p₁ ∈ P.precoverage.coverings Y
have change : F.presieve₀ ∈ P.precoverage.coverings Y
Tactic: change F.presieve₀ ∈ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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) ⋯
⊢ F.presieve₀ ∈ P.precoverage.coverings Y
have rw : P.property (PreZeroHypercover.pullback₁ g E)
Tactic: rw [F.presieve₀_mem_precoverage_iff, (P (X := Y)).prop_iff_of_iso e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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)
have refine : P.property E
Tactic: refine h₂ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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 E
have rwa : E.presieve₀ ∈ P.precoverage.coverings S
Tactic: rwa [← E.presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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
have refine_1 : P.property E
Tactic: refine (E.bind F).presieve₀_mem_precoverage_iff.mpr (h _ _ ?_ fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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
⊢ (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
have refine_2 : ∀ (i : E.I₀), P.property (F i)
Tactic: refine (E.bind F).presieve₀_mem_precoverage_iff.mpr (h _ _ ?_ fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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 }
⊢ P.property E
have refine_1 : E.presieve₀ ∈ P.precoverage.coverings S
Tactic: rwa [← E.presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
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₀
⊢ P.property (F i)
have refine_2 : Membership.mem (γ := Set (Presieve.{v, u} (E.X i))) (P.precoverage.coverings (E.X i)) (F i).presieve₀
Tactic: rw [← (F i).presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
R S : Presieve.{v, u} X
hR : R ∈ P.precoverage.coverings X
hS : S ∈ P.precoverage.coverings X
⊢ R ⊔ S ∈ P.precoverage.coverings X
have obtain : ∀ (E : PreZeroHypercover X) (hR : E.presieve₀ ∈ P.precoverage.coverings X), E.presieve₀ ⊔ S ∈ P.precoverage.coverings X
Tactic: obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
S : Presieve.{v, u} X
hS : S ∈ P.precoverage.coverings X
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
⊢ E.presieve₀ ⊔ S ∈ P.precoverage.coverings X
have obtain : ∀ (F : PreZeroHypercover X) (hS : F.presieve₀ ∈ P.precoverage.coverings X),
  E.presieve₀ ⊔ F.presieve₀ ∈ P.precoverage.coverings X
Tactic: obtain ⟨F, rfl⟩ := S.exists_eq_preZeroHypercover
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
F : PreZeroHypercover X
hS : F.presieve₀ ∈ P.precoverage.coverings X
⊢ E.presieve₀ ⊔ F.presieve₀ ∈ P.precoverage.coverings X
have rw : (E.sum F).presieve₀ ∈ P.precoverage.coverings X
Tactic: rw [← PreZeroHypercover.presieve₀_sum]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
F : PreZeroHypercover X
hS : F.presieve₀ ∈ P.precoverage.coverings X
⊢ (E.sum F).presieve₀ ∈ P.precoverage.coverings X
have rw : ∀ (hR : P.property E) (F : PreZeroHypercover X) (hS : P.property F), P.property (E.sum F)
Tactic: rw [PreZeroHypercover.presieve₀_mem_precoverage_iff] at hR hS ⊢
Cleared hypotheses: hR, F, hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
X Y : C
f : X ⟶ Y
x : P.obj (op X)
Z : C
g : Z ⟶ Y
hg : singleton f g
⊢ Z = X
have mk : X = X
Tactic: cases hg
Cleared hypotheses: Z, g, hg