awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
x : F.multicospanShape.R
dsimp :
  CategoryStruct.comp (Y :=
      WalkingMulticospan.right
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2)
          (f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).1),
            f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).2))
          (f.hom.s₁ (f.inv.s₁ (x.snd (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2))))))
      (WalkingMulticospan.Hom.snd
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2)
          (f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).1),
            f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).2))
          (f.hom.s₁ (f.inv.s₁ (x.snd (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2))))))
      (eqToHom ⋯) =
    eqToHom ⋯ ≫ WalkingMulticospan.Hom.snd x
⊢ Eq (α :=
    (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left (F.multicospanShape.snd x)) ⟶
      Functor.obj (𝟭 (WalkingMulticospan F.multicospanShape)) (WalkingMulticospan.right x))
    ((Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).map (WalkingMulticospan.Hom.snd x) ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ Functor.map (𝟭 (WalkingMulticospan F.multicospanShape)) (WalkingMulticospan.Hom.snd x))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
x : F.multicospanShape.R
w :
  Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2)
      (f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).1),
        f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).2))
      (f.hom.s₁ (f.inv.s₁ (x.snd (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2)))) =
    x
⊢ CategoryStruct.comp (Y :=
      WalkingMulticospan.right
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2)
          (f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).1),
            f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).2))
          (f.hom.s₁ (f.inv.s₁ (x.snd (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2))))))
      (WalkingMulticospan.Hom.snd
        (Sigma.mk (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2)
          (f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).1),
            f.hom.s₀ (f.inv.s₀ x.fst (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2).2))
          (f.hom.s₁ (f.inv.s₁ (x.snd (β := fun (i : F.I₀ × F.I₀) ↦ F.I₁ i.1 i.2))))))
      (eqToHom ⋯) =
    eqToHom ⋯ ≫ WalkingMulticospan.Hom.snd x

Tactic:
rw [eqToHom_naturality]

Premises used: CategoryTheory.eqToHom_naturality
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
c : WalkingMulticospan E.multicospanShape
left :
  ∀ (a : E.multicospanShape.L),
    (Hom.mapMulticospan f.hom).map (NatTrans.app (Iso.hom (eqToIso ⋯)) (WalkingMulticospan.left a)) ≫
        NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a)) =
      𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a))
right :
  ∀ (a : E.multicospanShape.R),
    (Hom.mapMulticospan f.hom).map (NatTrans.app (Iso.hom (eqToIso ⋯)) (WalkingMulticospan.right a)) ≫
        NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a)) =
      𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a))
⊢ (Hom.mapMulticospan f.hom).map (NatTrans.app (Iso.hom (eqToIso ⋯)) c) ≫
      NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj c) =
    𝟙 ((Hom.mapMulticospan f.hom).obj c)

Tactic:
cases c
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
a : E.multicospanShape.L
left :
  eqToHom ⋯ ≫ NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a))
⊢ (Hom.mapMulticospan f.hom).map (NatTrans.app (Iso.hom (eqToIso ⋯)) (WalkingMulticospan.left a)) ≫
      NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a))

Tactic:
rw [eqToIso.hom, eqToHom_app, eqToHom_map]

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
a : E.multicospanShape.R
right :
  eqToHom ⋯ ≫ NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a))
⊢ (Hom.mapMulticospan f.hom).map (NatTrans.app (Iso.hom (eqToIso ⋯)) (WalkingMulticospan.right a)) ≫
      NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a))

Tactic:
rw [eqToIso.hom, eqToHom_app, eqToHom_map]

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
a : E.multicospanShape.L
⊢ eqToHom ⋯ ≫ NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
a : E.multicospanShape.R
⊢ eqToHom ⋯ ≫ NatTrans.app (Iso.hom (eqToIso ⋯)) ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
refine : IsLimit (E.multifork G) ≃ IsLimit (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G))
⊢ IsLimit (E.multifork G) ≃ IsLimit (F.multifork G)

Tactic:
refine Equiv.trans ?_
    (IsLimit.whiskerEquivalenceEquiv <| PreOneHypercover.equivalenceMulticospanOfIso f).symm

Premises used: Equiv.trans, CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso, CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv, Equiv.symm
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
refine_1 :
  (E.multicospanIndex G).multicospan ≅ (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan
refine_2 :
  Functor.obj
      (Cone.postcompose
        (Iso.hom
          (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
            (fun (i : E.multicospanShape.R) ↦
              G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
            ⋯ ⋯)))
      (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)
⊢ IsLimit (E.multifork G) ≃ IsLimit (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G))

Tactic:
refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_

Premises used: CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
refine_1 :
  (i : E.multicospanShape.L) →
    (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.left i) ≅
      ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.left i)
refine_1₁ :
  (i : E.multicospanShape.R) →
    (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.right i) ≅
      ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.right i)
refine_1₂ :
  ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.fst i) ≫
        (G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op).hom =
      Iso.hom (G.mapIso (Iso.op (Iso.symm (asIso (f.hom.h₀ (E.multicospanShape.fst i)))))) ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.fst i)
refine_1₃ :
  ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.snd i) ≫
        (G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op).hom =
      Iso.hom (G.mapIso (Iso.op (Iso.symm (asIso (f.hom.h₀ (E.multicospanShape.snd i)))))) ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.snd i)
⊢ (E.multicospanIndex G).multicospan ≅ (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan

Tactic:
refine WalkingMulticospan.functorExt ?_ ?_ ?_ ?_

Premises used: CategoryTheory.Limits.WalkingMulticospan.functorExt
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
i : E.multicospanShape.L
⊢ (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.left i) ≅
    ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.left i)

Tactic:
exact G.mapIso (asIso (f.hom.h₀ i)).symm.op

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, CategoryTheory.Iso.op, CategoryTheory.PreOneHypercover.Hom.toHom, CategoryTheory.Iso.symm, CategoryTheory.Iso.hom, CategoryTheory.Functor.mapIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
i : E.multicospanShape.R
⊢ (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.right i) ≅
    ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.right i)

Tactic:
exact G.mapIso (asIso (f.hom.h₁ i.2)).symm.op

Premises used: CategoryTheory.Iso.op, CategoryTheory.Iso.symm, CategoryTheory.PreOneHypercover.Hom.h₁, Sigma.snd, CategoryTheory.Iso.hom, CategoryTheory.Functor.mapIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.fst i) ≫
        (G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op).hom =
      Iso.hom (G.mapIso (Iso.op (Iso.symm (asIso (f.hom.h₀ (E.multicospanShape.fst i)))))) ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.fst i)

Tactic:
simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₁]

Premises used: CategoryTheory.op_comp, CategoryTheory.PreOneHypercover.Hom.w₁₁, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.snd i) ≫
        (G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op).hom =
      Iso.hom (G.mapIso (Iso.op (Iso.symm (asIso (f.hom.h₀ (E.multicospanShape.snd i)))))) ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.snd i)

Tactic:
simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₂]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.PreOneHypercover.Hom.w₁₂, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
refine_2 :
  ∀ (i : WalkingMulticospan E.multicospanShape),
    NatTrans.app
        (Cone.π
          (Functor.obj
            (Cone.postcompose
              (Iso.hom
                (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                  (fun (i : E.multicospanShape.R) ↦
                    G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                  ⋯ ⋯)))
            (E.multifork G)))
        i =
      Iso.hom
          (Iso.refl
            (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
              (Functor.obj
                (Cone.postcompose
                  (Iso.hom
                    (WalkingMulticospan.functorExt
                      (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                      (fun (i : E.multicospanShape.R) ↦
                        G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                      ⋯ ⋯)))
                (E.multifork G)))) ≫
        (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app i
⊢ Functor.obj
      (Cone.postcompose
        (Iso.hom
          (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
            (fun (i : E.multicospanShape.R) ↦
              G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
            ⋯ ⋯)))
      (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)

Tactic:
refine Cone.ext (Iso.refl _) fun i ↦ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
a : E.multicospanShape.L
⊢ Eq (α :=
    Functor.obj.{w, v_1, w, u_1}
        (Functor.obj (Functor.const (WalkingMulticospan E.multicospanShape))
          (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
            (Functor.obj
              (Cone.postcompose
                (Iso.hom
                  (WalkingMulticospan.functorExt
                    (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                    (fun (i : E.multicospanShape.R) ↦
                      G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                    ⋯ ⋯)))
              (E.multifork G))))
        (WalkingMulticospan.left a) ⟶
      ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.left a))
    (NatTrans.app
      (Cone.π
        (Functor.obj
          (Cone.postcompose
            (Iso.hom
              (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                (fun (i : E.multicospanShape.R) ↦
                  G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                ⋯ ⋯)))
          (E.multifork G)))
      (WalkingMulticospan.left a))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
            (Functor.obj
              (Cone.postcompose
                (Iso.hom
                  (WalkingMulticospan.functorExt
                    (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                    (fun (i : E.multicospanShape.R) ↦
                      G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                    ⋯ ⋯)))
              (E.multifork G)))) ≫
      (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app (WalkingMulticospan.left a))

Tactic:
simp [← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
a : E.multicospanShape.R
⊢ Eq (α :=
    Functor.obj.{w, v_1, w, u_1}
        (Functor.obj (Functor.const (WalkingMulticospan E.multicospanShape))
          (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
            (Functor.obj
              (Cone.postcompose
                (Iso.hom
                  (WalkingMulticospan.functorExt
                    (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                    (fun (i : E.multicospanShape.R) ↦
                      G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                    ⋯ ⋯)))
              (E.multifork G))))
        (WalkingMulticospan.right a) ⟶
      ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.right a))
    (NatTrans.app
      (Cone.π
        (Functor.obj
          (Cone.postcompose
            (Iso.hom
              (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                (fun (i : E.multicospanShape.R) ↦
                  G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                ⋯ ⋯)))
          (E.multifork G)))
      (WalkingMulticospan.right a))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
            (Functor.obj
              (Cone.postcompose
                (Iso.hom
                  (WalkingMulticospan.functorExt
                    (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                    (fun (i : E.multicospanShape.R) ↦
                      G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                    ⋯ ⋯)))
              (E.multifork G)))) ≫
      (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app (WalkingMulticospan.right a))

Tactic:
simp [← Functor.map_comp, ← op_comp, f.hom.w₁₁_assoc]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
⊢ ∀ (i : G.I₀),
    CategoryStruct.comp (Y := (E.inter F).X (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i))
        (PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) i)
        ((E.inter F).f (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) i)) =
      G.f i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
i j : G.I₀
k : G.I₁ i j
rw : G.p₁ k ≫ f.h₀ i ≫ E.f (__spread.0.s₀ i).1 = G.p₁ k ≫ g.h₀ i ≫ F.f (__spread.0.s₀ i).2
⊢ f.h₁ k ≫ E.p₁ (f.s₁ k, g.s₁ k).1 ≫ E.f (__spread.0.s₀ i).1 =
    g.h₁ k ≫ F.p₁ (f.s₁ k, g.s₁ k).2 ≫ F.f (__spread.0.s₀ i).2

Tactic:
rw [f.w₁₁_assoc k, g.w₁₁_assoc k]

Premises used: CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
i j : G.I₀
k : G.I₁ i j
⊢ G.p₁ k ≫ f.h₀ i ≫ E.f (__spread.0.s₀ i).1 = G.p₁ k ≫ g.h₀ i ≫ F.f (__spread.0.s₀ i).2

Tactic:
simp