Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ((E.sigmaOfIsColimit hc hd).multifork F).pt ≅
    ((MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
                (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
                (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).symm.functor.obj
        (E.forkOfIsColimit hc hd F)).pt

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i ≅
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).left
        i

pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i ≅
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).right
        i

pp: case refine_4
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).fst i ≫ Iso.hom (?refine_3 i) =
      Iso.hom (?refine_2 ((E.sigmaOfIsColimit hc hd).multicospanShape.fst i)) ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).fst
          i

pp: case refine_5
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).snd i ≫ Iso.hom (?refine_3 i) =
      Iso.hom (?refine_2 ((E.sigmaOfIsColimit hc hd).multicospanShape.snd i)) ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).snd
          i

pp: case refine_6
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L),
    Iso.hom ?refine_1 ≫
        Multifork.ι
          ((MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).symm.functor.obj
            (E.forkOfIsColimit hc hd F))
          i =
      ((E.sigmaOfIsColimit hc hd).multifork F).ι i ≫ Iso.hom (?refine_2 i)

Tactic:
· exact .refl _

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i ≅
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).left
        i

case refine_3
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R) →
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i ≅
      (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
            (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).right
        i

case refine_4
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).fst i ≫ Iso.hom (?refine_3 i) =
      Iso.hom (?refine_2 ((E.sigmaOfIsColimit hc hd).multicospanShape.fst i)) ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).fst
          i

case refine_5
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).snd i ≫ Iso.hom (?refine_3 i) =
      Iso.hom (?refine_2 ((E.sigmaOfIsColimit hc hd).multicospanShape.snd i)) ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).snd
          i

case refine_6
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L),
    (Iso.refl ((E.sigmaOfIsColimit hc hd).multifork F).pt).hom ≫
        Multifork.ι
          ((MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).symm.functor.obj
            (E.forkOfIsColimit hc hd F))
          i =
      ((E.sigmaOfIsColimit hc hd).multifork F).ι i ≫ Iso.hom (?refine_2 i)