[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X✝ Y✝ : SimplexCategoryᵒᵖ
g : X✝ ⟶ Y✝
⊢ ∀ (j : Fin (SimplexCategory.len Y✝.unop + 1)),
    (fun i => WidePullback.π (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g.unop) i)) j ≫ f.hom =
      WidePullback.base fun x => f.hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePullback f✝.right (fun x => f✝.left) fun x => f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
inst✝ : ∀ (n : ℕ), HasWidePullback g.right (fun x => g.left) fun x => g.hom
F : f ⟶ g
n : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len n.unop + 1)
⊢ (fun i => WidePullback.π (fun x => f.hom) i ≫ F.left) j ≫ g.hom = (WidePullback.base fun x => f.hom) ≫ F.right
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : X ⟶ Arrow.augmentedCechNerve F
⊢ (𝟭 C).map (NatTrans.app G.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
[PROOFSTEP]
have := G.w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : X ⟶ Arrow.augmentedCechNerve F
this : (𝟭 (SimplicialObject C)).map G.left ≫ (Arrow.augmentedCechNerve F).hom = X.hom ≫ (const C).map G.right
⊢ (𝟭 C).map (NatTrans.app G.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
[PROOFSTEP]
apply_fun fun e => e.app (Opposite.op <| SimplexCategory.mk 0) at this 
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : X ⟶ Arrow.augmentedCechNerve F
this :
  NatTrans.app ((𝟭 (SimplicialObject C)).map G.left ≫ (Arrow.augmentedCechNerve F).hom)
      (Opposite.op (SimplexCategory.mk 0)) =
    NatTrans.app (X.hom ≫ (const C).map G.right) (Opposite.op (SimplexCategory.mk 0))
⊢ (𝟭 C).map (NatTrans.app G.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin (SimplexCategory.len x.unop + 1)
⊢ (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom = NatTrans.app X.hom x ≫ G.right
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin (SimplexCategory.len x.unop + 1)
⊢ (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right
[PROOFSTEP]
erw [Category.assoc, Arrow.w, Augmented.toArrow_obj_hom, NatTrans.naturality_assoc, Functor.const_obj_map,
  Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
⊢ ∀ ⦃X_1 Y : SimplexCategoryᵒᵖ⦄ (f : X_1 ⟶ Y),
    X.left.map f ≫
        (fun x =>
            WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
              (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
              (_ :
                ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                  (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                    NatTrans.app X.hom x ≫ G.right))
          Y =
      (fun x =>
            WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
              (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
              (_ :
                ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                  (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                    NatTrans.app X.hom x ≫ G.right))
          X_1 ≫
        (Arrow.augmentedCechNerve F).left.map f
[PROOFSTEP]
intro x y f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ X.left.map f ≫
      (fun x =>
          WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
            (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
            (_ :
              ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                  NatTrans.app X.hom x ≫ G.right))
        y =
    (fun x =>
          WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
            (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
            (_ :
              ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                  NatTrans.app X.hom x ≫ G.right))
        x ≫
      (Arrow.augmentedCechNerve F).left.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ X.left.map f ≫
      WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
        (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
        (_ :
          ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
            (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right) =
    WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
        (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
        (_ :
          ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
            (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
      WidePullback.lift (WidePullback.base fun x => F.hom)
        (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
            WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
              WidePullback.base fun x => F.hom)
[PROOFSTEP]
ext
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin (SimplexCategory.len y.unop + 1)
⊢ (X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.π (fun x => F.hom) j✝ =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.π (fun x => F.hom) j✝
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin (SimplexCategory.len y.unop + 1)
⊢ (X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.π (fun x => F.hom) j✝ =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.π (fun x => F.hom) j✝
[PROOFSTEP]
simp only [WidePullback.lift_π, Category.assoc, ← X.left.map_comp_assoc]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin (SimplexCategory.len y.unop + 1)
⊢ X.left.map (f ≫ (SimplexCategory.const y.unop j✝).op) ≫ G.left =
    X.left.map (SimplexCategory.const x.unop (↑(SimplexCategory.Hom.toOrderHom f.unop) j✝)).op ≫ G.left
[PROOFSTEP]
rfl
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ ((X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.base fun x => F.hom) =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.base fun x => F.hom
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ ((X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.base fun x => F.hom) =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.base fun x => F.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
⊢ Function.LeftInverse (equivalenceRightToLeft X F) (equivalenceLeftToRight X F)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F A) = A
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)).left = A.left
[PROOFSTEP]
dsimp
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ WidePullback.lift (NatTrans.app X.hom (Opposite.op (SimplexCategory.mk 0)) ≫ A.right)
        (fun i => X.left.map (SimplexCategory.const (SimplexCategory.mk 0) i).op ≫ A.left)
        (_ :
          ∀ (i : Fin (SimplexCategory.len (Opposite.op (SimplexCategory.mk 0)).unop + 1)),
            (fun i => X.left.map (SimplexCategory.const (Opposite.op (SimplexCategory.mk 0)).unop i).op ≫ A.left) i ≫
                F.hom =
              NatTrans.app X.hom (Opposite.op (SimplexCategory.mk 0)) ≫ A.right) ≫
      WidePullback.π (fun x => F.hom) 0 =
    A.left
[PROOFSTEP]
erw [WidePullback.lift_π]
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ X.left.map (SimplexCategory.const (SimplexCategory.mk 0) 0).op ≫ A.left = A.left
[PROOFSTEP]
nth_rw 2 [← Category.id_comp A.left]
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ X.left.map (SimplexCategory.const (SimplexCategory.mk 0) 0).op ≫ A.left = 𝟙 (Augmented.toArrow.obj X).left ≫ A.left
[PROOFSTEP]
congr 1
[GOAL]
case h₁.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ X.left.map (SimplexCategory.const (SimplexCategory.mk 0) 0).op = 𝟙 (Augmented.toArrow.obj X).left
[PROOFSTEP]
convert X.left.map_id _
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (SimplexCategory.const (SimplexCategory.mk 0) 0).op = 𝟙 (Opposite.op (SimplexCategory.mk 0))
[PROOFSTEP]
rw [← op_id]
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (SimplexCategory.const (SimplexCategory.mk 0) 0).op = (𝟙 (SimplexCategory.mk 0)).op
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_2.h.h.e'_8.e_f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ SimplexCategory.const (SimplexCategory.mk 0) 0 = 𝟙 (SimplexCategory.mk 0)
[PROOFSTEP]
ext ⟨a, ha⟩
[GOAL]
case h.e'_2.h.h.e'_8.e_f.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
a : ℕ
ha : a < SimplexCategory.len (SimplexCategory.mk 0) + 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change a < 1 at ha 
[GOAL]
case h.e'_2.h.h.e'_8.e_f.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
a : ℕ
ha : a < 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change 0 = a
[GOAL]
case h.e'_2.h.h.e'_8.e_f.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
a : ℕ
ha : a < 1
⊢ 0 = a
[PROOFSTEP]
linarith
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)).right = A.right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
⊢ Function.RightInverse (equivalenceRightToLeft X F) (equivalenceLeftToRight X F)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
⊢ equivalenceLeftToRight X F (equivalenceRightToLeft X F A) = A
[PROOFSTEP]
ext x : 2
[GOAL]
case h₁.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
⊢ NatTrans.app (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left x = NatTrans.app A.left x
[PROOFSTEP]
refine' WidePullback.hom_ext _ _ _ (fun j => _) _
[GOAL]
case h₁.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len x.unop + 1)
⊢ NatTrans.app (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left x ≫ WidePullback.π (fun x => F.hom) j =
    NatTrans.app A.left x ≫ WidePullback.π (fun x => F.hom) j
[PROOFSTEP]
dsimp
[GOAL]
case h₁.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len x.unop + 1)
⊢ WidePullback.lift (NatTrans.app X.hom x ≫ A.right)
        (fun i =>
          X.left.map (SimplexCategory.const x.unop i).op ≫
            NatTrans.app A.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0)
        (_ :
          ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
            (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ (equivalenceRightToLeft X F A).left) i ≫ F.hom =
              NatTrans.app X.hom x ≫ (equivalenceRightToLeft X F A).right) ≫
      WidePullback.π (fun x => F.hom) j =
    NatTrans.app A.left x ≫ WidePullback.π (fun x => F.hom) j
[PROOFSTEP]
simp
[GOAL]
case h₁.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len x.unop + 1)
⊢ NatTrans.app A.left x ≫
      WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const x.unop j)) 0) =
    NatTrans.app A.left x ≫ WidePullback.π (fun x => F.hom) j
[PROOFSTEP]
rfl
[GOAL]
case h₁.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
⊢ (NatTrans.app (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left x ≫ WidePullback.base fun x => F.hom) =
    NatTrans.app A.left x ≫ WidePullback.base fun x => F.hom
[PROOFSTEP]
simpa using congr_app A.w.symm x
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).right = A.right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    ↑(cechNerveEquiv X' Y).symm (f ≫ g) = Augmented.toArrow.map f ≫ ↑(cechNerveEquiv X Y).symm g
[PROOFSTEP]
dsimp [cechNerveEquiv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    equivalenceRightToLeft X' Y (f ≫ g) = Augmented.toArrow.map f ≫ equivalenceRightToLeft X Y g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    ↑(cechNerveEquiv X Y') (f ≫ g) = ↑(cechNerveEquiv X Y) f ≫ augmentedCechNerve.map g
[PROOFSTEP]
dsimp [cechNerveEquiv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    equivalenceLeftToRight X Y' (f ≫ g) = equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
x y : SimplexCategory
g : x ⟶ y
⊢ (fun n => widePushout f.left (fun x => f.right) fun x => f.hom) x ⟶
    (fun n => widePushout f.left (fun x => f.right) fun x => f.hom) y
[PROOFSTEP]
refine'
  WidePushout.desc (WidePushout.head _) (fun i => (@WidePushout.ι _ _ _ _ _ (fun _ => f.hom) ?_ (g.toOrderHom i)))
    (fun j => _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
x y : SimplexCategory
g : x ⟶ y
j : Fin (SimplexCategory.len x + 1)
⊢ f.hom ≫ (fun i => WidePushout.ι (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g) i)) j =
    WidePushout.head fun x => f.hom
[PROOFSTEP]
erw [← WidePushout.arrow_ι]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x => f✝.right) fun x => f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x => g.right) fun x => g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (SimplexCategory.len n + 1)
⊢ g.right ⟶ (cechConerve g).obj n
[PROOFSTEP]
apply WidePushout.ι _ i
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x => f✝.right) fun x => f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x => g.right) fun x => g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (SimplexCategory.len n + 1)
⊢ f.hom ≫ (fun i => F.right ≫ WidePushout.ι (fun x => g.hom) i) i = F.left ≫ WidePushout.head fun x => g.hom
[PROOFSTEP]
rw [← Arrow.w_assoc F, ← WidePushout.arrow_ι]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ (𝟭 C).map G.left ≫ (Augmented.toArrow.obj X).hom =
    F.hom ≫ (𝟭 C).map (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app G.right (SimplexCategory.mk 0))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) =
    F.hom ≫ WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app G.right (SimplexCategory.mk 0)
[PROOFSTEP]
rw [@WidePushout.arrow_ι_assoc _ _ _ _ _ (fun (_ : Fin 1) => F.hom) (by dsimp; infer_instance)]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ HasWidePushout ((𝟭 C).obj F.left) (fun x => (𝟭 C).obj F.right) fun x => F.hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ HasWidePushout F.left (fun x => F.right) fun x => F.hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app G.right (SimplexCategory.mk 0)
[PROOFSTEP]
exact congr_app G.w (SimplexCategory.mk 0)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
⊢ ∀ (j : Fin (SimplexCategory.len x + 1)),
    F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
rintro j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
rw [← Arrow.w_assoc G]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ G.left ≫ (Augmented.toArrow.obj X).hom ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
have t := X.hom.naturality (x.const j)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
t :
  ((const C).obj X.left).map (SimplexCategory.const x j) ≫ NatTrans.app X.hom x =
    NatTrans.app X.hom (SimplexCategory.mk 0) ≫ ((𝟭 (CosimplicialObject C)).obj X.right).map (SimplexCategory.const x j)
⊢ G.left ≫ (Augmented.toArrow.obj X).hom ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
t :
  𝟙 X.left ≫ NatTrans.app X.hom x = NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j)
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j) =
    G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
simp only [Category.id_comp] at t 
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
t : NatTrans.app X.hom x = NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j)
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j) =
    G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
rw [← t]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
⊢ ∀ ⦃X_1 Y : SimplexCategory⦄ (f : X_1 ⟶ Y),
    (Arrow.augmentedCechConerve F).right.map f ≫
        (fun x =>
            WidePushout.desc (G.left ≫ NatTrans.app X.hom x)
              (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
              (_ :
                ∀ (j : Fin (SimplexCategory.len x + 1)),
                  F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j =
                    G.left ≫ NatTrans.app X.hom x))
          Y =
      (fun x =>
            WidePushout.desc (G.left ≫ NatTrans.app X.hom x)
              (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
              (_ :
                ∀ (j : Fin (SimplexCategory.len x + 1)),
                  F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j =
                    G.left ≫ NatTrans.app X.hom x))
          X_1 ≫
        X.right.map f
[PROOFSTEP]
intro x y f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ (Arrow.augmentedCechConerve F).right.map f ≫
      (fun x =>
          WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
            (_ :
              ∀ (j : Fin (SimplexCategory.len x + 1)),
                F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x))
        y =
    (fun x =>
          WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
            (_ :
              ∀ (j : Fin (SimplexCategory.len x + 1)),
                F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x))
        x ≫
      X.right.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ WidePushout.desc (WidePushout.head fun x => F.hom)
        (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
              WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len y + 1)),
            F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
      X.right.map f
[PROOFSTEP]
ext
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
simp only [WidePushout.ι_desc_assoc, WidePushout.ι_desc]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ G.right ≫ X.right.map (SimplexCategory.const y (↑(SimplexCategory.Hom.toOrderHom f) j✝)) =
    (G.right ≫ X.right.map (SimplexCategory.const x j✝)) ≫ X.right.map f
[PROOFSTEP]
rw [Category.assoc, ← X.right.map_comp]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ G.right ≫ X.right.map (SimplexCategory.const y (↑(SimplexCategory.Hom.toOrderHom f) j✝)) =
    G.right ≫ X.right.map (SimplexCategory.const x j✝ ≫ f)
[PROOFSTEP]
rfl
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
simp only [Functor.const_obj_map, ← NatTrans.naturality, WidePushout.head_desc_assoc, WidePushout.head_desc,
  Category.assoc]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ G.left ≫ NatTrans.app X.hom y = G.left ≫ 𝟙 X.left ≫ NatTrans.app X.hom y
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
⊢ Function.LeftInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
⊢ equivalenceRightToLeft F X (equivalenceLeftToRight F X A) = A
[PROOFSTEP]
ext x : 2
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
⊢ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).left = A.left
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ NatTrans.app (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right x = NatTrans.app A.right x
[PROOFSTEP]
refine' WidePushout.hom_ext _ _ _ (fun j => _) _
[GOAL]
case h₂.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right x =
    WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app A.right x
[PROOFSTEP]
dsimp
[GOAL]
case h₂.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j ≫
      WidePushout.desc (A.left ≫ NatTrans.app X.hom x)
        (fun i =>
          (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app A.right (SimplexCategory.mk 0)) ≫
            X.right.map (SimplexCategory.const x i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ (fun i => (equivalenceLeftToRight F X A).right ≫ X.right.map (SimplexCategory.const x i)) j =
              (equivalenceLeftToRight F X A).left ≫ NatTrans.app X.hom x) =
    WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app A.right x
[PROOFSTEP]
simp only [Category.assoc, ← NatTrans.naturality A.right, Arrow.augmentedCechConerve_right, SimplexCategory.len_mk,
  Arrow.cechConerve_map, colimit.ι_desc, WidePushoutShape.mkCocone_ι_app, colimit.ι_desc_assoc]
[GOAL]
case h₂.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const x j)) 0) ≫
      NatTrans.app A.right x =
    WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app A.right x
[PROOFSTEP]
rfl
[GOAL]
case h₂.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x => F.hom) ≫ NatTrans.app (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right x =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app A.right x
[PROOFSTEP]
dsimp
[GOAL]
case h₂.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (A.left ≫ NatTrans.app X.hom x)
        (fun i =>
          (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app A.right (SimplexCategory.mk 0)) ≫
            X.right.map (SimplexCategory.const x i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ (fun i => (equivalenceLeftToRight F X A).right ≫ X.right.map (SimplexCategory.const x i)) j =
              (equivalenceLeftToRight F X A).left ≫ NatTrans.app X.hom x) =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app A.right x
[PROOFSTEP]
rw [colimit.ι_desc]
[GOAL]
case h₂.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ NatTrans.app
      (WidePushoutShape.mkCocone (A.left ≫ NatTrans.app X.hom x)
          (fun i =>
            (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app A.right (SimplexCategory.mk 0)) ≫
              X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => (equivalenceLeftToRight F X A).right ≫ X.right.map (SimplexCategory.const x i)) j =
                (equivalenceLeftToRight F X A).left ≫ NatTrans.app X.hom x)).ι
      none =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app A.right x
[PROOFSTEP]
exact congr_app A.w x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
⊢ Function.RightInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ equivalenceLeftToRight F X (equivalenceRightToLeft F X A) = A
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)).left = A.left
[PROOFSTEP]
rfl
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)).right = A.right
[PROOFSTEP]
dsimp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ WidePushout.ι (fun x => F.hom) 0 ≫
      WidePushout.desc (A.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0))
        (fun i => A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (SimplexCategory.mk 0) + 1)),
            F.hom ≫ (fun i => A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) i)) j =
              A.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0)) =
    A.right
[PROOFSTEP]
erw [WidePushout.ι_desc]
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) 0) = A.right
[PROOFSTEP]
nth_rw 2 [← Category.comp_id A.right]
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) 0) = A.right ≫ 𝟙 (Augmented.toArrow.obj X).right
[PROOFSTEP]
congr 1
[GOAL]
case h₂.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) 0) = 𝟙 (Augmented.toArrow.obj X).right
[PROOFSTEP]
convert X.right.map_id _
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ SimplexCategory.const (SimplexCategory.mk 0) 0 = 𝟙 (SimplexCategory.mk 0)
[PROOFSTEP]
ext ⟨a, ha⟩
[GOAL]
case h.e'_2.h.h.e'_8.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < SimplexCategory.len (SimplexCategory.mk 0) + 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change a < 1 at ha 
[GOAL]
case h.e'_2.h.h.e'_8.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change 0 = a
[GOAL]
case h.e'_2.h.h.e'_8.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < 1
⊢ 0 = a
[PROOFSTEP]
linarith
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ (wideCospan ι X).obj none)
[PROOFSTEP]
dsimp [wideCospan]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ ⊤_ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i j : WidePullbackShape ι
f : i ⟶ j
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map f ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        j =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        i ≫
      (wideCospan ι X).map f
[PROOFSTEP]
cases f
[GOAL]
case id
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i : WidePullbackShape ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id i) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        i =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        i ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id i)
[PROOFSTEP]
cases i
[GOAL]
case id.none
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id none) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id none)
case id.some
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id (some val✝)) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id (some val✝))
[PROOFSTEP]
all_goals dsimp; simp
[GOAL]
case id.none
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id none) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id none)
[PROOFSTEP]
dsimp
[GOAL]
case id.none
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ 𝟙 (∏ fun x => X) ≫ terminal.from (∏ fun x => X) = terminal.from (∏ fun x => X) ≫ (wideCospan ι X).map (𝟙 none)
[PROOFSTEP]
simp
[GOAL]
case id.some
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id (some val✝)) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id (some val✝))
[PROOFSTEP]
dsimp
[GOAL]
case id.some
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : ι
⊢ 𝟙 (∏ fun x => X) ≫ limit.π (Discrete.functor fun x => X) { as := val✝ } =
    limit.π (Discrete.functor fun x => X) { as := val✝ } ≫ (wideCospan ι X).map (𝟙 (some val✝))
[PROOFSTEP]
simp
[GOAL]
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.term j✝) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some j✝) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
[PROOFSTEP]
dsimp
[GOAL]
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ 𝟙 (∏ fun x => X) ≫ terminal.from (∏ fun x => X) =
    limit.π (Discrete.functor fun x => X) { as := j✝ } ≫ (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
[PROOFSTEP]
simp only [terminal.comp_from]
[GOAL]
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ terminal.from (∏ fun x => X) =
    limit.π (Discrete.functor fun x => X) { as := j✝ } ≫ (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
⊢ f = (fun s => Pi.lift fun j => NatTrans.app s.π (some j)) s
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
⊢ f = Pi.lift fun j => NatTrans.app s.π (some j)
[PROOFSTEP]
ext j
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j = (Pi.lift fun j => NatTrans.app s.π (some j)) ≫ Pi.π (fun x => X) j
[PROOFSTEP]
dsimp only [Limits.Pi.lift]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j =
    limit.lift (Discrete.functor fun b => X) (Fan.mk s.pt fun j => NatTrans.app s.π (some j)) ≫ Pi.π (fun x => X) j
[PROOFSTEP]
rw [limit.lift_π]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j = NatTrans.app (Fan.mk s.pt fun j => NatTrans.app s.π (some j)).π { as := j }
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j = NatTrans.app s.π (some j)
[PROOFSTEP]
rw [← h (some j)]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ HasWidePullback (Arrow.mk (terminal.from X)).right (fun x => (Arrow.mk (terminal.from X)).left) fun x =>
    (Arrow.mk (terminal.from X)).hom
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : Fintype ι
⊢ HasWidePullback (Arrow.mk (terminal.from X)).right (fun x => (Arrow.mk (terminal.from X)).left) fun x =>
    (Arrow.mk (terminal.from X)).hom
[PROOFSTEP]
exact ⟨⟨wideCospan.limitCone ι X⟩⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j : ι
⊢ (limitIsoPi ι X).hom ≫ Pi.π (fun x => X) j = WidePullback.π (fun x => terminal.from X) j
[PROOFSTEP]
rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
⊢ (Arrow.cechNerve (Arrow.mk (terminal.from X))).map f ≫
      ((fun m => wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left)
          n).hom =
    ((fun m => wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left) m).hom ≫
      (cechNerveTerminalFrom X).map f
[PROOFSTEP]
dsimp only [cechNerveTerminalFrom, Arrow.cechNerve]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
⊢ WidePullback.lift (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
        (fun i =>
          WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                (Arrow.mk (terminal.from X)).hom =
              WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom) ≫
      (wideCospan.limitIsoPi (Fin (SimplexCategory.len n.unop + 1)) (Arrow.mk (terminal.from X)).left).hom =
    (wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
      Pi.lift fun i => Pi.π (fun x => X) (↑(SimplexCategory.Hom.toOrderHom f.unop) i)
[PROOFSTEP]
ext ⟨j⟩
[GOAL]
case h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
j : ℕ
isLt✝ : j < SimplexCategory.len n.unop + 1
⊢ (WidePullback.lift (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
          (fun i =>
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
              WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                  (Arrow.mk (terminal.from X)).hom =
                WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom) ≫
        (wideCospan.limitIsoPi (Fin (SimplexCategory.len n.unop + 1)) (Arrow.mk (terminal.from X)).left).hom) ≫
      Pi.π (fun x => X) { val := j, isLt := isLt✝ } =
    ((wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
        Pi.lift fun i => Pi.π (fun x => X) (↑(SimplexCategory.Hom.toOrderHom f.unop) i)) ≫
      Pi.π (fun x => X) { val := j, isLt := isLt✝ }
[PROOFSTEP]
simp only [Category.assoc, limit.lift_π, Fan.mk_π_app]
[GOAL]
case h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
j : ℕ
isLt✝ : j < SimplexCategory.len n.unop + 1
⊢ WidePullback.lift (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
        (fun i =>
          WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                (Arrow.mk (terminal.from X)).hom =
              WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom) ≫
      (wideCospan.limitIsoPi (Fin (SimplexCategory.len n.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
        Pi.π (fun x => X) { val := j, isLt := isLt✝ } =
    (wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
      Pi.π (fun x => X) (↑(SimplexCategory.Hom.toOrderHom f.unop) { val := j, isLt := isLt✝ })
[PROOFSTEP]
erw [wideCospan.limitIsoPi_hom_comp_pi, wideCospan.limitIsoPi_hom_comp_pi, limit.lift_π]
[GOAL]
case h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
j : ℕ
isLt✝ : j < SimplexCategory.len n.unop + 1
⊢ NatTrans.app
      (WidePullbackShape.mkCone (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
          (fun i =>
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
              WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                  (Arrow.mk (terminal.from X)).hom =
                WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)).π
      (some { val := j, isLt := isLt✝ }) =
    WidePullback.π (fun x => terminal.from X) (↑(SimplexCategory.Hom.toOrderHom f.unop) { val := j, isLt := isLt✝ })
[PROOFSTEP]
rfl
