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_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.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₀ (𝟙 (pullback₂ f E)) 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:
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.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₀ (𝟙 (pullback₂ f E)) i

Tactic:
simp
-- 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_1 F : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{w'', v, u} S
inst_1 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
i : (E.inter F).I₀
⊢ pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            I₀.{w', v, u} (C := C) (S := E.X i) ((fun (i : E.I₀) ↦ pullback₁ (E.f i) F) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.1) :
                (a : E.I₀ × F.1) → (E.bind fun (i : E.I₀) ↦ pullback₁ (E.f i) F).I₀)
              i)))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            I₀.{w', v, u} (C := C) (S := E.X i) ((fun (i : E.I₀) ↦ pullback₁ (E.f i) F) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.1) :
                (a : E.I₀ × F.1) → (E.bind fun (i : E.I₀) ↦ pullback₁ (E.f i) F).I₀)
              i))) ≫
      F.f i.2 =
    (E.inter F).f i

Tactic:
simp [← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- 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_1 F : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{w'', v, u} S
inst_1 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
f : G.Hom E
g : G.Hom F
i : G.I₀
⊢ f.h₀ i ≫
      E.f
        (Sigma.fst (β := fun (i : E.I₀) ↦
          I₀.{w', v, u} (C := C) (S := E.X i) ((fun (i : E.I₀) ↦ pullback₁ (E.f i) F) i))
          ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.1) :
              (a : E.I₀ × F.1) → (E.bind fun (i : E.I₀) ↦ pullback₁ (E.f i) F).I₀)
            (f.s₀ i, g.s₀ i))) =
    g.h₀ i ≫
      F.f
        (Sigma.snd (β := fun (i : E.I₀) ↦
          I₀.{w', v, u} (C := C) (S := E.X i) ((fun (i : E.I₀) ↦ pullback₁ (E.f i) F) i))
          ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.1) :
              (a : E.I₀ × F.1) → (E.bind fun (i : E.I₀) ↦ pullback₁ (E.f i) F).I₀)
            (f.s₀ i, g.s₀ i)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
R : Presieve.{v, u} S
⊢ R.preZeroHypercover.presieve₀ = R

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
R : Presieve.{v, u} S
refine_1 : R.preZeroHypercover.presieve₀ ≤ R
refine_2 : R ≤ R.preZeroHypercover.presieve₀
⊢ R.preZeroHypercover.presieve₀ = R

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
R : Presieve.{v, u} S
Y : C
i : R.preZeroHypercover.I₀
⊢ R (R.preZeroHypercover.f i)

Tactic:
i.2

Premises used: CategoryTheory.Presieve.uncurry, Set.Mem, setOf, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
R : Presieve.{v, u} S
Y : C
i : R.preZeroHypercover.I₀
⊢ R (R.preZeroHypercover.f i)

Tactic:
exact i.2

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
R : Presieve.{v, u} S
Y : C
f : Y ⟶ S
h : R f
i : (↑R.uncurry : Type (max u v)) :=
  Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ R.uncurry) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Y f) h
⊢ R.preZeroHypercover.presieve₀ f

Tactic:
.mk i

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
R : Presieve.{v, u} S
Y : C
f : Y ⟶ S
h : R f
i : (↑R.uncurry : Type (max u v)) :=
  Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ R.uncurry) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Y f) h
⊢ R.preZeroHypercover.presieve₀ f

Tactic:
exact .mk i
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
R : Presieve.{v, u} S
⊢ R = R.preZeroHypercover.presieve₀

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
⊢ E.shrink.presieve₀ = E.presieve₀

Tactic:
E.presieve₀.presieve₀_preZeroHypercover

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, CategoryTheory.Presieve.presieve₀_preZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
h : E.presieve₀ = F.presieve₀
rw : E.presieve₀.preZeroHypercover = F.shrink
rw₁ : E.presieve₀.preZeroHypercover = F.presieve₀.preZeroHypercover
rw₂ rw₃ : F.presieve₀.preZeroHypercover = F.presieve₀.preZeroHypercover
⊢ E.shrink = F.shrink

Tactic:
rw [shrink, shrink, h]

Premises used: CategoryTheory.PreZeroHypercover.shrink
-- 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.presieve₀ = F.presieve₀ ↔ E.shrink = F.shrink

Tactic:
⟨fun h ↦ shrink_eq_shrink_of_presieve₀_eq_presieve₀ h, fun h ↦ ?_⟩

Premises used: Iff.intro, CategoryTheory.PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
refine : ∀ (h : E.shrink = F.shrink), E.presieve₀ = F.presieve₀
⊢ E.presieve₀ = F.presieve₀ ↔ E.shrink = F.shrink

Tactic:
refine ⟨fun h ↦ shrink_eq_shrink_of_presieve₀_eq_presieve₀ h, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreZeroHypercover.{w, v, u} S
h : E.shrink = F.shrink
rw : E.shrink.presieve₀ = F.presieve₀
rw₁ : E.shrink.presieve₀ = F.shrink.presieve₀
rw₂ rw₃ : F.shrink.presieve₀ = F.shrink.presieve₀
⊢ E.presieve₀ = F.presieve₀

Tactic:
rw [← E.presieve₀_shrink, ← F.presieve₀_shrink, h]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_shrink
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hRT : ∀ ⦃Z : C⦄ (g : Z ⟶ S), R g → ∃ (Y : C) (e : Y ≅ Z), T (e.hom ≫ g)
hTR : ∀ ⦃Z : C⦄ (g : Z ⟶ S), T g → ∃ (Y : C) (e : Y ≅ Z), R (e.hom ≫ g)
hR : R ∈ J.coverings S
choose :
  ∀ (YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C) (eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z)
    (hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)), T ∈ J.coverings S
⊢ T ∈ J.coverings S

Tactic:
choose YR eR hTeg using hRT
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hTR : ∀ ⦃Z : C⦄ (g : Z ⟶ S), T g → ∃ (Y : C) (e : Y ≅ Z), R (e.hom ≫ g)
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
choose :
  ∀ (YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C) (eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z)
    (hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)), T ∈ J.coverings S
⊢ T ∈ J.coverings S

Tactic:
choose YT eT hReg using hTR
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
i_1 : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))
i : (↑R.uncurry : Type (max u v))
⊢ Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
      (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
      (Sum.inl i) ⟶
    S

Tactic:
exact i.1.2

Premises used: Sigma.snd, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
i_1 : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))
i : (↑T.uncurry : Type (max u v))
⊢ Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
      (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
      (Sum.inr i) ⟶
    S

Tactic:
exact (eT _ i.2).hom ≫ i.1.2

Premises used: Sigma.snd, Subtype.val, CategoryTheory.Iso.hom, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))
i : (↑R.uncurry : Type (max u v))
⊢ Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
      (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) (Sum.inl i) ⟶
    S

Tactic:
exact (eR _ i.2).hom ≫ i.1.2

Premises used: Sigma.snd, Subtype.val, CategoryTheory.Iso.hom, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))
i : (↑T.uncurry : Type (max u v))
⊢ Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
      (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) (Sum.inr i) ⟶
    S

Tactic:
exact i.1.2

Premises used: Sigma.snd, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑R.uncurry : Type (max u v))
dsimp :
  (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S) ≅
    YR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯
⊢ E.X (Sum.inl i) ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) (Sum.inl i))

Tactic:
dsimp [E, F]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑R.uncurry : Type (max u v))
symm :
  YR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯ ≅
    (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)
⊢ (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S) ≅
    YR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.RespectsIso
S : C
R T : Presieve.{v, u} S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim (fun (j : (↑R.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S))
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ YT ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              i ⟶
            S)
        i with
      | Sum.inl i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i =>
        Iso.hom (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
F : PreZeroHypercover S :=
  { I₀ := (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v)),
    X := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      Sum.elim
        (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
        (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i,
    f := fun (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) ↦
      match (motive :=
        (i : (↑R.uncurry : Type (max u v)) ⊕ (↑T.uncurry : Type (max u v))) →
          Sum.elim
              (fun (j : (↑R.uncurry : Type (max u v))) ↦ YR ((↑j : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯)
              (fun (j : (↑T.uncurry : Type (max u v))) ↦ (↑j : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)) i ⟶
            S)
        i with
      | Sum.inl i =>
        Iso.hom (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) ≫
          (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)
      | Sum.inr i => (↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S) }
i_1 : E.I₀
i : (↑R.uncurry : Type (max u v))
⊢ YR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯ ≅
    (↑i : (Y : C) × (Y ⟶ S)).fst (β := fun (Y : C) ↦ Y ⟶ S)

Tactic:
exact eR _ _