awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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)
have 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
Tactic: refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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
⊢ (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
have 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
Tactic: simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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 =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ d'.proj i
have 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
Tactic: rw [MulticospanIndex.fstPiMapOfIsLimit_proj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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)
have 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
Tactic: refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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
⊢ (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
have 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
Tactic: simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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 =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ d'.proj i
have 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
Tactic: rw [MulticospanIndex.sndPiMapOfIsLimit_proj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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)
have 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
Tactic: refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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
⊢ (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
have refine_3 : (E.forkOfIsColimit hc hd F).ι ≫ c'.proj i = F.map (E.f i).op
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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
⊢ IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃ IsLimit (E.multifork F)
have refine_1 : ((E.sigmaOfIsColimit hc hd).multifork F).pt ≅
  Cone.pt.{w, v_1, w, u_1} (J := WalkingMulticospan (E.sigmaOfIsColimit hc hd).multicospanShape)
    (Functor.obj
      (Equivalence.functor
        (Equivalence.symm
          (MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
            (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)))
            (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.forkOfIsColimit hc hd F))
Tactic: refine (Multifork.isLimitEquivOfIsos _ _ ?_ ?_ ?_ ?_ ?_ ?_).trans
    (IsLimit.ofConeEquiv <| (MulticospanIndex.multiforkOfParallelHomsEquivFork
      (E.sigmaOfIsColimit hc hd).multicospanShape _ _).symm) |>.trans
      (E.isLimitMultiforkEquivIsLimitFork hc hd F).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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
refine_1 :
  ((E.sigmaOfIsColimit hc hd).multifork F).pt ≅
    Cone.pt.{w, v_1, w, u_1} (J := WalkingMulticospan (E.sigmaOfIsColimit hc hd).multicospanShape)
      (Functor.obj
        (Equivalence.functor
          (Equivalence.symm
            (MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
              (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)))
              (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.forkOfIsColimit hc hd F))
⊢ IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃ IsLimit (E.multifork F)
have refine_2 : (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L) →
  ((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i ≅
    MulticospanIndex.left
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape (X := F.obj (op 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)))
        (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))))
      i
Tactic: refine (Multifork.isLimitEquivOfIsos _ _ ?_ ?_ ?_ ?_ ?_ ?_).trans
    (IsLimit.ofConeEquiv <| (MulticospanIndex.multiforkOfParallelHomsEquivFork
      (E.sigmaOfIsColimit hc hd).multicospanShape _ _).symm) |>.trans
      (E.isLimitMultiforkEquivIsLimitFork hc hd F).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S W : C
p : W ⟶ S
⊢ Eq (α := Sieve.{v, u} W) (sieve₁ (trivial S) (i₁ := PUnit.unit) (i₂ := PUnit.unit) p p) ⊤
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ W), Sieve.arrows (sieve₁ (trivial S) (i₁ := PUnit.unit) (i₂ := PUnit.unit) p p) f ↔ Sieve.arrows ⊤ f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
⊢ (E.inter F).sieve₁ p₁ p₂ =
    Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
      fun (x : C) (f : x ⟶ W)
        (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ W),
  ((E.inter F).sieve₁ p₁ p₂).arrows f ↔
    (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
          fun (x : C) (f : x ⟶ W)
            (x_1 :
              (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
          Sieve.pullback f
            (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
      f
Tactic: ext Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f ↔
    (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
          fun (x : C) (f : x ⟶ W)
            (x_1 :
              (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
          Sieve.pullback f
            (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
      f
have h : ((E.inter F).sieve₁ p₁ p₂).arrows f →
  ∀ (k : (E.inter F).I₁ i j) (a : Y ⟶ (E.inter F).Y k) (h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k)
    (h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k),
    (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
          fun (x : C) (f : x ⟶ W)
            (x_1 :
              (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
          Sieve.pullback f
            (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
      f
Tactic: refine ⟨fun ⟨k, a, h₁, h₂⟩ ↦ ?_, fun ⟨Z, a, b, ⟨k, e, h₁, h₂⟩, ⟨l, u, u₁, u₂⟩, hab⟩ ↦ ?_⟩