awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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

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₀
⊢ Hom.h₀
      ({ 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₀ := ⋯ })
      i =
    Hom.h₀ (𝟙 E) 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
h :
  ∀ (x : F.I₀),
    Hom.s₀
        ({ 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₀ := ⋯ } ≫
          { s₀ := (⇑s₀ : (a : E.I₀) → F.I₀), h₀ := fun (i : E.I₀) ↦ (h₀ i).hom, w₀ := ⋯ : E.Hom F })
        x =
      Hom.s₀ (𝟙 F) x
⊢ Hom.s₀
      ({ 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₀ := ⋯ } ≫
        { s₀ := (⇑s₀ : (a : E.I₀) → F.I₀), h₀ := fun (i : E.I₀) ↦ (h₀ i).hom, w₀ := ⋯ : E.Hom F }) =
    Hom.s₀ (𝟙 F)

Tactic:
ext
-- 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
x : F.I₀
⊢ Hom.s₀
      ({ 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₀ := ⋯ } ≫
        { s₀ := (⇑s₀ : (a : E.I₀) → F.I₀), h₀ := fun (i : E.I₀) ↦ (h₀ i).hom, w₀ := ⋯ : E.Hom F })
      x =
    Hom.s₀ (𝟙 F) x

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₀
⊢ Hom.h₀
      ({ 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₀ := ⋯ } ≫
        { s₀ := (⇑s₀ : (a : E.I₀) → F.I₀), h₀ := fun (i : E.I₀) ↦ (h₀ i).hom, w₀ := ⋯ : E.Hom F })
      i =
    Hom.h₀ (𝟙 F) i ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ e.inv.s₀ (e.hom.s₀ i) = i

Tactic:
congr($(e.hom_inv_id).s₀ i)

Premises used: congrArg, CategoryTheory.Iso.hom_inv_id, id, CategoryTheory.PreZeroHypercover.Hom.s₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ e.hom.s₀ (e.inv.s₀ i) = i

Tactic:
congr($(e.inv_hom_id).s₀ i)

Premises used: CategoryTheory.Iso.inv_hom_id, congrArg, id, CategoryTheory.PreZeroHypercover.Hom.s₀
-- 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.79917, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ E.X i = E.X (e.inv.s₀ (e.hom.s₀ i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ (e.hom ≫ e.inv).s₀ = Hom.s₀ (𝟙 E)

Tactic:
obtain ⟨hs, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreZeroHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = Hom.s₀ (𝟙 E)
⊢ ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = Hom.h₀ (𝟙 E) i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreZeroHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = Hom.s₀ (𝟙 E)
hh : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = Hom.h₀ (𝟙 E) i ≫ eqToHom ⋯
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯

Tactic:
simpa using hh 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_1 : PreZeroHypercover.{w', v, u} S
E_2 : PreZeroHypercover.{w, v, u} S
F_2 : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{?u.82039, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ F.X i = F.X (e.hom.s₀ (e.inv.s₀ i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ (e.inv ≫ e.hom).s₀ = Hom.s₀ (𝟙 F)

Tactic:
obtain ⟨hs, hh⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreZeroHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = Hom.s₀ (𝟙 F)
⊢ ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = Hom.h₀ (𝟙 F) i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, hh⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreZeroHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = Hom.s₀ (𝟙 F)
hh : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = Hom.h₀ (𝟙 F) i ≫ eqToHom ⋯
⊢ e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom ⋯

Tactic:
simpa using hh 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_1 : PreZeroHypercover.{w', v, u} S
E_2 : PreZeroHypercover.{w, v, u} S
F_2 : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{?u.84161, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ E.X (e.inv.s₀ (e.hom.s₀ i)) = E.X i

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_1 : PreZeroHypercover.{w', v, u} S
E_2 : PreZeroHypercover.{w, v, u} S
F_2 : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{?u.84161, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
h :
  e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ = 𝟙 (E.X i) ∧
    (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))
⊢ IsIso (e.hom.h₀ i)

Tactic:
use e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom (by simp)

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, CategoryTheory.eqToHom, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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.84161, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
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
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.84161, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
h :
  Eq.{v + 1} (α := E.X i ⟶ E.X i) (𝟙 (E.X i)) (𝟙 (E.X i)) ∧
    Eq.{v + 1} (α := F.X (e.hom.s₀ i) ⟶ F.X (e.hom.s₀ i)) (eqToHom ⋯ ≫ eqToHom ⋯) (𝟙 (F.X (e.hom.s₀ i)))
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ = 𝟙 (E.X i) ∧
    (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))

Tactic:
rw [hom_inv_h₀_assoc, eqToHom_trans, eqToHom_refl, Category.assoc,
    ← eqToHom_naturality _ (by simp), inv_hom_h₀_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_refl, CategoryTheory.PreZeroHypercover.inv_hom_h₀_assoc, CategoryTheory.PreZeroHypercover.hom_inv_h₀_assoc, CategoryTheory.eqToHom_naturality, CategoryTheory.eqToHom_trans
-- 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.84161, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ Eq.{v + 1} (α := E.X i ⟶ E.X i) (𝟙 (E.X i)) (𝟙 (E.X i)) ∧
    Eq.{v + 1} (α := F.X (e.hom.s₀ i) ⟶ F.X (e.hom.s₀ i)) (eqToHom ⋯ ≫ eqToHom ⋯) (𝟙 (F.X (e.hom.s₀ i)))

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_1 : PreZeroHypercover.{w', v, u} S
E_2 : PreZeroHypercover.{w, v, u} S
F_2 : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{?u.87640, v, u} S
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ IsIso (e.inv.h₀ i)

Tactic:
.of_isIso_fac_right (inv_hom_h₀ e i)

Premises used: CategoryTheory.PreZeroHypercover.inv_hom_h₀, CategoryTheory.IsIso.of_isIso_fac_right
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ inv (e.hom.h₀ i) ≫ E.f i = F.f (e.hom.s₀ i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ inv (e.inv.h₀ i) ≫ F.f i = E.f (e.inv.s₀ i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_1, v, u} S
F : PreZeroHypercover.{u_2, v, u} S
f : E.Hom F
rw : ∀ (i : E.I₀), F.sieve₀.arrows (E.f i)
⊢ E.sieve₀ ≤ F.sieve₀

Tactic:
rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff, CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_1, v, u} S
F : PreZeroHypercover.{u_2, v, u} S
f : E.Hom F
i : E.I₀
rw : F.sieve₀.arrows (f.h₀ i ≫ F.f (f.s₀ i))
⊢ F.sieve₀.arrows (E.f i)

Tactic:
rw [← f.w₀ i]

Premises used: CategoryTheory.PreZeroHypercover.Hom.w₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_1, v, u} S
F : PreZeroHypercover.{u_2, v, u} S
f : E.Hom F
i : E.I₀
x : F.sieve₀.arrows (Y := F.X (f.s₀ i)) (F.f (f.s₀ i))
⊢ F.sieve₀.arrows (f.h₀ i ≫ F.f (f.s₀ i))

Tactic:
apply Sieve.downward_closed

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_1, v, u} S
F : PreZeroHypercover.{u_2, v, u} S
f : E.Hom F
i : E.I₀
⊢ F.sieve₀.arrows (Y := F.X (f.s₀ i)) (F.f (f.s₀ i))

Tactic:
Sieve.le_generate _ _ _ ⟨f.s₀ i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Sieve.le_generate, CategoryTheory.PreZeroHypercover.Hom.s₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{u_1, v, u} S
F : PreZeroHypercover.{u_2, v, u} S
f : E.Hom F
i : E.I₀
⊢ F.sieve₀.arrows (Y := F.X (f.s₀ i)) (F.f (f.s₀ i))

Tactic:
exact Sieve.le_generate _ _ _ ⟨f.s₀ i⟩

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{u_1, v, u} S
e : E ≅ F
⊢ E.sieve₀ = F.sieve₀

Tactic:
le_antisymm e.hom.sieve₀_le_sieve₀ e.inv.sieve₀_le_sieve₀

Premises used: le_antisymm, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.PreZeroHypercover.Hom.sieve₀_le_sieve₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ presieve₀.{w, v_1, u_1} (map F E) = Presieve.map F E.presieve₀

Tactic:
(Presieve.map_ofArrows _).symm

Premises used: CategoryTheory.Presieve.map_ofArrows, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
⊢ sieve₀.{w, v_1, u_1} (map F E) = Sieve.functorPushforward F E.sieve₀

Tactic:
simp [← Sieve.generate_map_eq_functorPushforward, Presieve.map_ofArrows, map]

Premises used: CategoryTheory.Presieve.map_ofArrows, CategoryTheory.PreZeroHypercover.map, CategoryTheory.Sieve.generate_map_eq_functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ Hom.s₀
      ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₁ f E).Hom (pullback₂ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ }) =
    Hom.s₀ (𝟙 (pullback₁ f E))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
apply :
  HEq (α :=
    (i : (pullback₁ f E).I₀) →
      (pullback₁ f E).X i ⟶
        (pullback₁ f E).X
          (Hom.s₀
            ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
                (pullback₁ f E).Hom (pullback₂ f E) } ≫
              { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ })
            i))
    (Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₁ f E).Hom (pullback₂ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ }))
    (Hom.h₀ (𝟙 (pullback₁ f E)))
⊢ { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
        (pullback₁ f E).Hom (pullback₂ f E) } ≫
      { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ } =
    𝟙 (pullback₁ f E)

Tactic:
apply Hom.ext (by rfl)

Premises used: CategoryTheory.PreZeroHypercover.Hom.ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
simp :
  Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₁ f E).Hom (pullback₂ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ }) =
    Hom.h₀ (𝟙 (pullback₁ f E))
⊢ HEq (α :=
    (i : (pullback₁ f E).I₀) →
      (pullback₁ f E).X i ⟶
        (pullback₁ f E).X
          (Hom.s₀
            ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
                (pullback₁ f E).Hom (pullback₂ f E) } ≫
              { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ })
            i))
    (Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₁ f E).Hom (pullback₂ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ }))
    (Hom.h₀ (𝟙 (pullback₁ f E)))

Tactic:
simp only [heq_eq_eq]

Premises used: heq_eq_eq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
h :
  ∀ (i : (pullback₁ f E).I₀),
    Hom.h₀
        ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
            (pullback₁ f E).Hom (pullback₂ f E) } ≫
          { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ })
        i =
      Hom.h₀ (𝟙 (pullback₁ f E)) i
⊢ Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₁ f E).Hom (pullback₂ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ }) =
    Hom.h₀ (𝟙 (pullback₁ f E))

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
i : (pullback₁ f E).I₀
⊢ Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₁ f E).Hom (pullback₂ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ })
      i =
    Hom.h₀ (𝟙 (pullback₁ f E)) i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ Hom.s₀
      ({ s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₂ f E).Hom (pullback₁ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ }) =
    Hom.s₀ (𝟙 (pullback₂ f E))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
apply :
  HEq (α :=
    (i : (pullback₂ f E).I₀) →
      (pullback₂ f E).X i ⟶
        (pullback₂ f E).X
          (Hom.s₀
            ({ s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
                (pullback₂ f E).Hom (pullback₁ f E) } ≫
              { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ })
            i))
    (Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₂ f E).Hom (pullback₁ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ }))
    (Hom.h₀ (𝟙 (pullback₂ f E)))
⊢ { s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
        (pullback₂ f E).Hom (pullback₁ f E) } ≫
      { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ } =
    𝟙 (pullback₂ f E)

Tactic:
apply Hom.ext (by rfl)

Premises used: CategoryTheory.PreZeroHypercover.Hom.ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S_1 T_1 : C
E_1 : PreZeroHypercover.{w, v, u} S_1
F : PreZeroHypercover.{w', v, u} S_1
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback f (E.f i)
inst_2 : ∀ (i : E.I₀), HasPullback (E.f i) f
simp :
  Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₂ f E).Hom (pullback₁ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ }) =
    Hom.h₀ (𝟙 (pullback₂ f E))
⊢ HEq (α :=
    (i : (pullback₂ f E).I₀) →
      (pullback₂ f E).X i ⟶
        (pullback₂ f E).X
          (Hom.s₀
            ({ s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
                (pullback₂ f E).Hom (pullback₁ f E) } ≫
              { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ })
            i))
    (Hom.h₀
      ({ s₀ := id, h₀ := fun (i : (pullback₂ f E).I₀) ↦ Iso.inv (pullbackSymmetry f (E.f i)), w₀ := ⋯ :
          (pullback₂ f E).Hom (pullback₁ f E) } ≫
        { s₀ := id, h₀ := fun (i : (pullback₁ f E).I₀) ↦ Iso.hom (pullbackSymmetry f (E.f i)), w₀ := ⋯ }))
    (Hom.h₀ (𝟙 (pullback₂ f E)))

Tactic:
simp only [heq_eq_eq]

Premises used: heq_eq_eq