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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ Iso.hom (Iso.refl c'.pt) ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)

Tactic:
Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
refine_1 :
  ∀ (i : E.multicospanShape.R),
    (Iso.hom (Iso.refl c'.pt) ≫
          F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))) ≫
        d'.proj i =
      ((E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)) ≫ d'.proj i
⊢ Iso.hom (Iso.refl c'.pt) ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)

Tactic:
refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
refine_1 :
  F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
      d'.proj i =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ d'.proj i
⊢ (Iso.hom (Iso.refl c'.pt) ≫
        F.map
          (Quiver.Hom.op
            (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
              E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))) ≫
      d'.proj i =
    ((E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)) ≫ d'.proj i

Tactic:
simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]

Premises used: CategoryTheory.PreOneHypercover.multicospanIndex_right, CategoryTheory.PreOneHypercover.multicospanShape_L, CategoryTheory.Category.comp_id, CategoryTheory.PreOneHypercover.multicospanShape_R, CategoryTheory.PreOneHypercover.Y'_apply, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
refine_1 :
  F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
      d'.proj i =
    c'.proj (E.multicospanShape.fst i) ≫ (E.multicospanIndex F).fst i
⊢ F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
      d'.proj i =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ d'.proj i

Tactic:
rw [MulticospanIndex.fstPiMapOfIsLimit_proj]

Premises used: CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj
-- 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
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
      d'.proj i =
    c'.proj (E.multicospanShape.fst i) ≫ (E.multicospanIndex F).fst i

Tactic:
simp [c', d', ← F.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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ Iso.hom (Iso.refl c'.pt) ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)

Tactic:
Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
refine_2 :
  ∀ (i : E.multicospanShape.R),
    (Iso.hom (Iso.refl c'.pt) ≫
          F.map
            (Quiver.Hom.op
              (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
                E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                  c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))) ≫
        d'.proj i =
      ((E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)) ≫ d'.proj i
⊢ Iso.hom (Iso.refl c'.pt) ≫
      F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)

Tactic:
refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
refine_2 :
  F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
      d'.proj i =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ d'.proj i
⊢ (Iso.hom (Iso.refl c'.pt) ≫
        F.map
          (Quiver.Hom.op
            (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
              E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
                c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))) ≫
      d'.proj i =
    ((E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ Iso.hom (Iso.refl d'.pt)) ≫ d'.proj i

Tactic:
simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]

Premises used: CategoryTheory.PreOneHypercover.multicospanIndex_right, CategoryTheory.PreOneHypercover.multicospanShape_L, CategoryTheory.Category.comp_id, CategoryTheory.PreOneHypercover.multicospanShape_R, CategoryTheory.PreOneHypercover.Y'_apply, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
refine_2 :
  F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
      d'.proj i =
    c'.proj (E.multicospanShape.snd i) ≫ (E.multicospanIndex F).snd i
⊢ F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
      d'.proj i =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ d'.proj i

Tactic:
rw [MulticospanIndex.sndPiMapOfIsLimit_proj]

Premises used: CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj
-- 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
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ F.map
        (Quiver.Hom.op
          (Cofan.IsColimit.desc hd fun (x : E.I₁') ↦
            E.p₂ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
              c.inj x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
      d'.proj i =
    c'.proj (E.multicospanShape.snd i) ≫ (E.multicospanIndex F).snd i

Tactic:
simp [c', d', ← F.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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ Iso.hom (Iso.refl (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)).pt) ≫
      (E.forkOfIsColimit hc hd F).ι =
    Fork.ι (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≫
      Iso.hom (Iso.refl c'.pt)

Tactic:
Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
refine_3 :
  ∀ (i : E.multicospanShape.L),
    (Iso.hom
            (Iso.refl (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)).pt) ≫
          (E.forkOfIsColimit hc hd F).ι) ≫
        c'.proj i =
      (Fork.ι (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≫
          Iso.hom (Iso.refl c'.pt)) ≫
        c'.proj i
⊢ Iso.hom (Iso.refl (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)).pt) ≫
      (E.forkOfIsColimit hc hd F).ι =
    Fork.ι (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≫
      Iso.hom (Iso.refl c'.pt)

Tactic:
refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_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 : PreOneHypercover.{w, v, u} S
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.L
refine_3 : (E.forkOfIsColimit hc hd F).ι ≫ c'.proj i = F.map (E.f i).op
⊢ (Iso.hom (Iso.refl (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)).pt) ≫
        (E.forkOfIsColimit hc hd F).ι) ≫
      c'.proj i =
    (Fork.ι (((E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').functor.obj (E.multifork F)) ≫
        Iso.hom (Iso.refl c'.pt)) ≫
      c'.proj 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
c : Cofan.{w, v, u} E.X
hc : IsColimit c
d : Cofan.{w, v, u} E.Y'
hd : IsColimit d
F : Functor.{v, v_1, u, u_1} Cᵒᵖ A
inst_2 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₀) (Discrete.functor fun (i : E.I₀) ↦ op (E.X i)) F
inst_3 : PreservesLimit.{w, w, v, v_1, u, u_1} (J := Discrete E.I₁') (Discrete.functor fun (i : E.I₁') ↦ op (E.Y' i)) F
c' : Fan.{w, v_1, u_1} (E.multicospanIndex F).left :=
  Fan.mk (F.obj (op c.pt)) fun (i : E.multicospanShape.L) ↦ F.map (c.inj i).op
hc' : IsLimit c' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₀) ↦ op (E.X i)) (fun (i : E.I₀) ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan.{w, v_1, u_1} (E.multicospanIndex F).right :=
  Fan.mk (F.obj (op d.pt)) fun (i : E.multicospanShape.R) ↦ F.map (d.inj i).op
hd' : IsLimit d' :=
  isLimitFanMkObjOfIsLimit F (fun (i : E.I₁') ↦ op (E.Y' i)) (fun (i : E.I₁') ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.L
⊢ (E.forkOfIsColimit hc hd F).ι ≫ c'.proj i = F.map (E.f i).op

Tactic:
simp [c']