awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
i : E.I₀
⊢ E.presieve₀ (E.f i)

Tactic:
⟨i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
i : E.I₀
⊢ 𝟙 (E.X i) ≫ E.f i = E.f i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
f : S ⟶ T
⊢ presieve₀.{u_1, v, u} (singleton f) = Presieve.singleton f

Tactic:
simp [singleton, presieve₀, Presieve.ofArrows_pUnit]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, CategoryTheory.PreZeroHypercover.singleton, CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
⊢ IsEmpty.{u_1 + 1} (I₀.{u_1, v, u} (empty S))

Tactic:
inferInstanceAs <| IsEmpty PEmpty

Premises used: _private.0.CategoryTheory.PreZeroHypercover.instIsEmptyI₀Empty._proof_1
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
⊢ Eq (α := Presieve.{v, u} S) (presieve₀.{w, v, u} (empty S)) ⊥

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ presieve₀.{w, v, u} (pullback₂ f E) = Presieve.pullbackArrows f E.presieve₀

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback (E.f i) f
refine_1 : presieve₀.{w, v, u} (pullback₂ f E) ≤ Presieve.pullbackArrows f E.presieve₀
refine_2 : Presieve.pullbackArrows f E.presieve₀ ≤ presieve₀.{w, v, u} (pullback₂ f E)
⊢ presieve₀.{w, v, u} (pullback₂ f E) = Presieve.pullbackArrows f E.presieve₀

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback (E.f i) f
Y : C
i : (pullback₂ f E).I₀
⊢ Presieve.pullbackArrows f E.presieve₀ ((pullback₂ f E).f i)

Tactic:
use _, _, i
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback (E.f i) f
Y_1 Y : C
i : E.I₀
⊢ (pullback₂ f E).presieve₀ (Y := pullback (E.f i) f) (pullback.snd (E.f i) f)

Tactic:
use i
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E_1 : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
X : C
E : PreZeroHypercover.{u_1, v, u} X
Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i ≫ f) g
i : E.I₀
⊢ (E.f i ≫ f) ≫ 𝟙 Z = E.f i ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E_1 : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
X : C
E : PreZeroHypercover.{u_1, v, u} X
Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i ≫ f) g
i : E.I₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E_1 : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Y : C
E : PreZeroHypercover.{w, v, u} Y
X Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
inst_2 : ∀ (i : E.I₀), HasPullback f (E.f i ≫ g)
i : E.I₀
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E_1 : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Y : C
E : PreZeroHypercover.{w, v, u} Y
X Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
inst_2 : ∀ (i : E.I₀), HasPullback f (E.f i ≫ g)
i : E.I₀
⊢ (E.f i ≫ g) ≫ 𝟙 Z = E.f i ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
⊢ presieve₀.{w', v, u} (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)) = E.presieve₀

Tactic:
le_antisymm (fun Y g ⟨i⟩ ↦ ⟨e i⟩) fun Y g ⟨i⟩ ↦ ?_

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, _private.0.CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_equiv.match_2, CategoryTheory.PreZeroHypercover.restrictIndex, le_antisymm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
refine :
  ∀ (Y : C) (g : Y ⟶ S),
    E.presieve₀ g → ∀ (i : E.I₀), (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (E.f i)
⊢ presieve₀.{w', v, u} (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)) = E.presieve₀

Tactic:
refine le_antisymm (fun Y g ⟨i⟩ ↦ ⟨e i⟩) fun Y g ⟨i⟩ ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
Y : C
g : Y ⟶ S
h : E.presieve₀ g
i : E.I₀
obtain :
  ∀ (i : ι),
    (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (Y := E.X ((e : (a : ι) → E.I₀) i))
      (E.f ((e : (a : ι) → E.I₀) i))
⊢ (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (E.f i)

Tactic:
obtain ⟨i, rfl⟩ := e.surjective i

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
Y : C
g : Y ⟶ S
h : E.presieve₀ g
i : ι
⊢ (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (Y := E.X ((e : (a : ι) → E.I₀) i))
    (E.f ((e : (a : ι) → E.I₀) i))

Tactic:
⟨i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
Y : C
g : Y ⟶ S
h : E.presieve₀ g
i : ι
⊢ (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (Y := E.X ((e : (a : ι) → E.I₀) i))
    (E.f ((e : (a : ι) → E.I₀) i))

Tactic:
exact ⟨i⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type u_1
f : ι → E.I₀
rw : ∀ (i : (E.restrictIndex f).I₀), E.presieve₀ ((E.restrictIndex f).f i)
⊢ presieve₀.{u_1, v, u} (E.restrictIndex f) ≤ E.presieve₀

Tactic:
rw [Presieve.ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type u_1
f : ι → E.I₀
i : (E.restrictIndex f).I₀
⊢ E.presieve₀ ((E.restrictIndex f).f i)

Tactic:
.mk _

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type u_1
f : ι → E.I₀
i : (E.restrictIndex f).I₀
⊢ E.presieve₀ ((E.restrictIndex f).f i)

Tactic:
exact .mk _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
⊢ presieve₀.{w', v, u} (E.reindex e) = E.presieve₀

Tactic:
simp [reindex]

Premises used: CategoryTheory.PreZeroHypercover.reindex
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
inst_1 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
⊢ E.inter F =
    (bind.{w', w, v, u} E fun (i : E.I₀) ↦ pullback₁ (E.f i) F).reindex (ι := Prod.{w, w'} E.I₀ F.1)
      (Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.1))

Tactic:
rfl

Premises used: CategoryTheory.PreZeroHypercover.inter, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
i : E.I₀
⊢ (E.sum F).X (Sum.inl i) = E.X i

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
i : F.I₀
⊢ (E.sum F).X (Sum.inr i) = F.X i

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
i : E.I₀
⊢ (E.sum F).f (Sum.inl i) = E.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
i : F.I₀
⊢ (E.sum F).f (Sum.inr i) = F.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
a : Presieve.ofArrows (E.sum F).X (E.sum F).f ≤ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f
a₁ : Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f ≤ Presieve.ofArrows (E.sum F).X (E.sum F).f
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f = Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
a : ∀ (i : (E.sum F).I₀), (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f i)
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f g ≤ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) g

Tactic:
⟨i⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
i : (E.sum F).I₀
a :
  ∀ (val : E.I₀),
    (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inl val)) ((E.sum F).f (Sum.inl val))
a₁ :
  ∀ (val : F.I₀),
    (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inr val)) ((E.sum F).f (Sum.inr val))
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f i)

Tactic:
cases i
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
val : E.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inl val)) ((E.sum F).f (Sum.inl val))

Tactic:
Or.inl (.mk _)

Premises used: CategoryTheory.Presieve.ofArrows.mk, Or.inl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
val : E.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inl val)) ((E.sum F).f (Sum.inl val))

Tactic:
exact Or.inl (.mk _)

Premises used: Or.inl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
val : F.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inr val)) ((E.sum F).f (Sum.inr val))

Tactic:
Or.inr (.mk _)

Premises used: CategoryTheory.Presieve.ofArrows.mk, Or.inr
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
val : F.I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inr val)) ((E.sum F).f (Sum.inr val))

Tactic:
exact Or.inr (.mk _)

Premises used: Or.inr
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Y : C
i : E.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (E.f i)

Tactic:
⟨Sum.inl i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sum.inl, Sum.elim
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Y : C
i : E.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (E.f i)

Tactic:
exact ⟨Sum.inl i⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)

Tactic:
⟨Sum.inr i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sum.inr, Sum.elim
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Y : C
i : F.I₀
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f (F.f i)

Tactic:
exact ⟨Sum.inr i⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
T : C
f : T ⟶ S
i : E.I₀
⊢ (E.add f).X (some i) = E.X i

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
T : C
f : T ⟶ S
⊢ (E.add f).X none = T

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
T : C
f : T ⟶ S
i : E.I₀
⊢ (E.add f).f (some i) = E.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
T : C
f : T ⟶ S
⊢ (E.add f).f none = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
T : C
f : T ⟶ S
⊢ presieve₀.{w, v, u} (E.add f) = E.presieve₀ ⊔ Presieve.singleton f

Tactic:
simp [add, presieve₀_reindex, presieve₀_sum]

Premises used: CategoryTheory.PreZeroHypercover.add, CategoryTheory.PreZeroHypercover.presieve₀_sum, CategoryTheory.PreZeroHypercover.presieve₀_reindex
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
i : E.I₀
r : PUnit.{w + 1}
⊢ c.inj i ≫ (E.sigmaOfIsColimit hc).f r = E.f i

Tactic:
simp [PreZeroHypercover.sigmaOfIsColimit]

Premises used: CategoryTheory.PreZeroHypercover.sigmaOfIsColimit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
⊢ presieve₀.{w, v, u} (E.sigmaOfIsColimit hc) = Presieve.singleton (Cofan.IsColimit.desc hc E.f)

Tactic:
Presieve.ofArrows_pUnit _

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E_1 : PreZeroHypercover.{w, v, u} S
F_1 : PreZeroHypercover.{w', v, u} S
E_2 : PreZeroHypercover.{w, v, u} S
F_2 : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{?u.60813, v, u} S
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
f g : E.Hom F
hs : f.s₀ = g.s₀
i : E.I₀
rw rw₁ : F.X (g.s₀ i) = F.X (g.s₀ i)
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)

Tactic:
rw [hs]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
f g : E.Hom F
hs : f.s₀ = g.s₀
hh : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
mk :
  ∀ (s₀ : (i : E.I₀) → F.I₀) (h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), h₀ i ≫ F.f (s₀ i) = E.f i)
    (hs : { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.s₀ = g.s₀)
    (hh : ∀ (i : E.I₀), { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.h₀ i = g.h₀ i ≫ eqToHom ⋯),
    { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
g : E.Hom F
s₀ : (i : E.I₀) → F.I₀
h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), h₀ i ≫ F.f (s₀ i) = E.f i
hs : { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.s₀ = g.s₀
hh : ∀ (i : E.I₀), { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.h₀ i = g.h₀ i ≫ eqToHom ⋯
mk :
  ∀ (s₀_1 : (i : E.I₀) → F.I₀) (h₀_1 : (i : E.I₀) → E.X i ⟶ F.X (s₀_1 i))
    (w₀_1 : ∀ (i : E.I₀), h₀_1 i ≫ F.f (s₀_1 i) = E.f i)
    (hs : { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.s₀ = { s₀ := s₀_1, h₀ := h₀_1, w₀ := w₀_1 }.s₀)
    (hh :
      ∀ (i : E.I₀),
        { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.h₀ i =
          { s₀ := s₀_1, h₀ := h₀_1, w₀ := w₀_1 : E.Hom F }.h₀ i ≫ eqToHom ⋯),
    { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F } = { s₀ := s₀_1, h₀ := h₀_1, w₀ := w₀_1 }
⊢ { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F } = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E_1 : PreZeroHypercover.{w, v, u} S
F_1 : PreZeroHypercover.{w', v, u} S
E_2 : PreZeroHypercover.{w, v, u} S
F_2 : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{?u.68465, v, u} S
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
f g : E.Hom F
hs : f.s₀ = g.s₀
i : E.I₀
rw rw₁ : F.X (g.s₀ i) = F.X (g.s₀ i)
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)

Tactic:
rw [hs]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
f g : E.Hom F
h : f = g
⊢ ∃ (hs : f.s₀ = f.s₀), ∀ (i : E.I₀), f.h₀ i = f.h₀ i ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F_1 : PreZeroHypercover.{w', v, u} S_1
E_2 : PreZeroHypercover.{w, v, u} S_1
F_2 : PreZeroHypercover.{w', v, u} S_1
G : PreZeroHypercover.{?u.70083, v, u} S_1
S : C
E F : PreZeroHypercover.{w, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
i : F.I₀
⊢ F.X i = F.X ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i : E.I₀))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F_1 : PreZeroHypercover.{w', v, u} S_1
E_2 : PreZeroHypercover.{w, v, u} S_1
F_2 : PreZeroHypercover.{w', v, u} S_1
G : PreZeroHypercover.{?u.70083, v, u} S_1
S : C
E F : PreZeroHypercover.{w, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
i : F.I₀
obtain :
  ∀ (i : E.I₀),
    Eq (α := F.X ((s₀ : (a : E.I₀) → F.I₀) i) ⟶ S)
      ((eqToHom ⋯ ≫ Iso.inv (h₀ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)))) ≫
        E.f ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)))
      (F.f ((s₀ : (a : E.I₀) → F.I₀) i))
⊢ (eqToHom ⋯ ≫ Iso.inv (h₀ ((s₀.symm : (a : F.I₀) → E.I₀) i))) ≫ E.f ((s₀.symm : (a : F.I₀) → E.I₀) i) = F.f i

Tactic:
obtain ⟨i, rfl⟩ := s₀.surjective i

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F_1 : PreZeroHypercover.{w', v, u} S_1
E_2 : PreZeroHypercover.{w, v, u} S_1
F_2 : PreZeroHypercover.{w', v, u} S_1
G : PreZeroHypercover.{?u.70083, v, u} S_1
S : C
E F : PreZeroHypercover.{w, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
i : E.I₀
simp : eqToHom ⋯ ≫ E.f ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)) = E.f i
⊢ Eq (α := F.X ((s₀ : (a : E.I₀) → F.I₀) i) ⟶ S)
    ((eqToHom ⋯ ≫ Iso.inv (h₀ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)))) ≫
      E.f ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)))
    (F.f ((s₀ : (a : E.I₀) → F.I₀) i))

Tactic:
simp only [← cancel_epi (h₀ i).hom, w₀, Category.assoc, Equiv.symm_apply_apply,
      eqToHom_iso_hom_naturality_assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_iso_hom_naturality_assoc, Equiv.symm_apply_apply, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F_1 : PreZeroHypercover.{w', v, u} S_1
E_2 : PreZeroHypercover.{w, v, u} S_1
F_2 : PreZeroHypercover.{w', v, u} S_1
G : PreZeroHypercover.{?u.70083, v, u} S_1
S : C
E F : PreZeroHypercover.{w, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
i : E.I₀
⊢ i = (s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F_1 : PreZeroHypercover.{w', v, u} S_1
E_2 : PreZeroHypercover.{w, v, u} S_1
F_2 : PreZeroHypercover.{w', v, u} S_1
G : PreZeroHypercover.{?u.70083, v, u} S_1
S : C
E F : PreZeroHypercover.{w, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
i : E.I₀
rw : E.f i ≫ eqToHom ⋯ = E.f i
⊢ eqToHom ⋯ ≫ E.f ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)) = E.f i

Tactic:
rw [← CategoryTheory.eqToHom_naturality _ (by simp)]

Premises used: CategoryTheory.eqToHom_naturality
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F_1 : PreZeroHypercover.{w', v, u} S_1
E_2 : PreZeroHypercover.{w, v, u} S_1
F_2 : PreZeroHypercover.{w', v, u} S_1
G : PreZeroHypercover.{?u.70083, v, u} S_1
S : C
E F : PreZeroHypercover.{w, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
i : E.I₀
⊢ E.f i ≫ eqToHom ⋯ = E.f i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F_1 : PreZeroHypercover.{w', v, u} S_1
E_2 : PreZeroHypercover.{w, v, u} S_1
F_2 : PreZeroHypercover.{w', v, u} S_1
G : PreZeroHypercover.{?u.70083, v, u} S_1
S : C
E F : PreZeroHypercover.{w, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
h :
  ∀ (x : E.I₀),
    Hom.s₀
        ({ s₀ := (⇑s₀ : (a : E.I₀) → F.I₀), h₀ := fun (i : E.I₀) ↦ (h₀ i).hom, w₀ := ⋯ : E.Hom F } ≫
          { s₀ := (⇑s₀.symm : (a : F.I₀) → E.I₀),
            h₀ := fun (i : F.I₀) ↦ eqToHom ⋯ ≫ Iso.inv (h₀ ((s₀.symm : (a : F.I₀) → E.I₀) i)), w₀ := ⋯ })
        x =
      Hom.s₀ (𝟙 E) x
⊢ Hom.s₀
      ({ s₀ := (⇑s₀ : (a : E.I₀) → F.I₀), h₀ := fun (i : E.I₀) ↦ (h₀ i).hom, w₀ := ⋯ : E.Hom F } ≫
        { s₀ := (⇑s₀.symm : (a : F.I₀) → E.I₀),
          h₀ := fun (i : F.I₀) ↦ eqToHom ⋯ ≫ Iso.inv (h₀ ((s₀.symm : (a : F.I₀) → E.I₀) i)), w₀ := ⋯ }) =
    Hom.s₀ (𝟙 E)

Tactic:
ext