-- 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) }
refine_1 : (i : E.I₀) → E.X i ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) i)
refine_2 :
  ∀ (i : E.I₀),
    CategoryStruct.comp (Y := F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) i))
        (Iso.hom
          ((fun (i : E.I₀) ↦
              (match (motive := (i : E.I₀) → E.X i ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) i)) i with
                | Sum.inl i => id (Iso.symm (eR ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯))
                | Sum.inr i => id (eT ((↑i : (Y : C) × (Y ⟶ S)).snd (β := fun (Y : C) ↦ Y ⟶ S)) ⋯) :
                E.X i ≅ F.X ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) i)))
            i))
        (F.f ((Equiv.refl E.I₀ : (a : E.I₀) → F.I₀) i)) =
      E.f i
⊢ E ≅ F

Tactic:
refine PreZeroHypercover.isoMk (Equiv.refl _) (fun i ↦ ?_) (fun i ↦ ?_)

Premises used: CategoryTheory.PreZeroHypercover.isoMk, Equiv.refl