awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
h₂ :
  WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
        (fun (x : Fin (x.len + 1)) ↦ F.hom)
        ((SimplexCategory.Hom.toOrderHom (⦋0⦌.const x j) : (a : Fin (0 + 1)) → Fin (x.len + 1)) 0) ≫
      A.right.app x =
    WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
        (fun (x : Fin (x.len + 1)) ↦ F.hom) j ≫
      A.right.app x
⊢ CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
        (fun (x : Fin (x.len + 1)) ↦ F.hom) j)
      (WidePushout.desc (A.left ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦
          CategoryStruct.comp (Y := X.right ^⦋0⦌)
            (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                (fun (x : Fin 1) ↦ F.hom) 0 ≫
              A.right.app ⦋0⦌)
            (X.right.map (⦋0⦌.const x i)))
        ⋯) =
    WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
        (fun (x : Fin (x.len + 1)) ↦ F.hom) j ≫
      A.right.app x

Tactic:
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]

Premises used: CategoryTheory.Category.assoc, SimplexCategory.len_mk, CategoryTheory.CommaMorphism.right, CategoryTheory.Limits.WidePushoutShape.mkCocone_ι_app, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.NatTrans.naturality, CategoryTheory.Arrow.augmentedCechConerve_right, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.Arrow.cechConerve_map
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
        (fun (x : Fin (x.len + 1)) ↦ F.hom)
        ((SimplexCategory.Hom.toOrderHom (⦋0⦌.const x j) : (a : Fin (0 + 1)) → Fin (x.len + 1)) 0) ≫
      A.right.app x =
    WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
        (fun (x : Fin (x.len + 1)) ↦ F.hom) j ≫
      A.right.app x

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
h₂ :
  CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.desc (A.left ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦
          CategoryStruct.comp (Y := X.right ^⦋0⦌)
            (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                (fun (x : Fin 1) ↦ F.hom) 0 ≫
              A.right.app ⦋0⦌)
            (X.right.map (⦋0⦌.const x i)))
        ⋯) =
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x
⊢ CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom :
        F.left ⟶ widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
      (NatTrans.app (CommaMorphism.right (equivalenceRightToLeft F X (equivalenceLeftToRight F X A))) x :
        F.augmentedCechConerve.right.obj x ⟶ X.right.obj x) =
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
h₂ :
  NatTrans.app
      (Cocone.ι
        (WidePushoutShape.mkCocone (A.left ≫ X.hom.app x)
          (fun (i : Fin (x.len + 1)) ↦
            CategoryStruct.comp (Y := X.right ^⦋0⦌)
              (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                  (fun (x : Fin 1) ↦ F.hom) 0 ≫
                A.right.app ⦋0⦌)
              (X.right.map (⦋0⦌.const x i)))
          ⋯))
      none =
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x
⊢ CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.desc (A.left ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦
          CategoryStruct.comp (Y := X.right ^⦋0⦌)
            (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                (fun (x : Fin 1) ↦ F.hom) 0 ≫
              A.right.app ⦋0⦌)
            (X.right.map (⦋0⦌.const x i)))
        ⋯) =
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x

Tactic:
rw [colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ NatTrans.app
      (Cocone.ι
        (WidePushoutShape.mkCocone (A.left ≫ X.hom.app x)
          (fun (i : Fin (x.len + 1)) ↦
            CategoryStruct.comp (Y := X.right ^⦋0⦌)
              (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                  (fun (x : Fin 1) ↦ F.hom) 0 ≫
                A.right.app ⦋0⦌)
              (X.right.map (⦋0⦌.const x i)))
          ⋯))
      none =
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x

Tactic:
congr_app A.w x

Premises used: CategoryTheory.Functor.id, CategoryTheory.CommaMorphism.w, CategoryTheory.Limits.colimit, CategoryTheory.Functor.const, CategoryTheory.Arrow, CategoryTheory.congr_app, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ NatTrans.app
      (Cocone.ι
        (WidePushoutShape.mkCocone (A.left ≫ X.hom.app x)
          (fun (i : Fin (x.len + 1)) ↦
            CategoryStruct.comp (Y := X.right ^⦋0⦌)
              (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                  (fun (x : Fin 1) ↦ F.hom) 0 ≫
                A.right.app ⦋0⦌)
              (X.right.map (⦋0⦌.const x i)))
          ⋯))
      none =
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x

Tactic:
exact congr_app A.w x

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h₁ : Arrow.Hom.left (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.left A
h₂ : Arrow.Hom.right (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.right A
⊢ equivalenceLeftToRight F X (equivalenceRightToLeft F X A) = A

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
⊢ Arrow.Hom.left (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.left A

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h₂ :
  CategoryStruct.comp (Y := widePushout.{0, v, u} F.left (fun (x : Fin 1) ↦ F.right) fun (x : Fin 1) ↦ F.hom)
      (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right) (fun (x : Fin 1) ↦ F.hom) 0)
      (WidePushout.desc (Arrow.Hom.left A ≫ X.hom.app ⦋0⦌)
        (fun (i : Fin 1) ↦ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ i)) ⋯) =
    Arrow.Hom.right A
⊢ Arrow.Hom.right (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.right A

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h₂ : Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A
⊢ CategoryStruct.comp (Y := widePushout.{0, v, u} F.left (fun (x : Fin 1) ↦ F.right) fun (x : Fin 1) ↦ F.hom)
      (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right) (fun (x : Fin 1) ↦ F.hom) 0)
      (WidePushout.desc (Arrow.Hom.left A ≫ X.hom.app ⦋0⦌)
        (fun (i : Fin 1) ↦ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ i)) ⋯) =
    Arrow.Hom.right A

Tactic:
rw [WidePushout.ι_desc]

Premises used: CategoryTheory.Limits.WidePushout.ι_desc
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h₂ : Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A ≫ 𝟙 (Functor.obj Augmented.toArrow X).right
⊢ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A

Tactic:
nth_rw 2 [← Category.comp_id A.right]

Premises used: CategoryTheory.Arrow.Hom.right, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h₂ : X.right.map (⦋0⦌.const ⦋0⦌ 0) = 𝟙 (Functor.obj Augmented.toArrow X).right
⊢ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A ≫ 𝟙 (Functor.obj Augmented.toArrow X).right

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
⊢ X.right.map (𝟙 ⦋0⦌) = 𝟙 (X.right ^⦋0⦌)

Tactic:
X.right.map_id _

Premises used: CategoryTheory.Comma.right, CategoryTheory.Functor.map_id
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h : ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌
⊢ X.right.map (⦋0⦌.const ⦋0⦌ 0) = 𝟙 (Functor.obj Augmented.toArrow X).right

Tactic:
convert! X.right.map_id _

Premises used: CategoryTheory.Comma.right, CategoryTheory.Functor.map_id
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h :
  ∀ (a : ℕ) (ha : a < ⦋0⦌.len + 1),
    (↑((SimplexCategory.Hom.toOrderHom (⦋0⦌.const ⦋0⦌ 0) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋0⦌.len + 1))
            (⟨a, ha⟩ : Fin (⦋0⦌.len + 1))) :
        ℕ) =
      (↑((SimplexCategory.Hom.toOrderHom (𝟙 ⦋0⦌) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋0⦌.len + 1)) ⟨a, ha⟩) : ℕ)
⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌

Tactic:
ext ⟨a, ha⟩
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
a : ℕ
ha : a < ⦋0⦌.len + 1
⊢ (↑((SimplexCategory.Hom.toOrderHom (⦋0⦌.const ⦋0⦌ 0) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋0⦌.len + 1))
          (⟨a, ha⟩ : Fin (⦋0⦌.len + 1))) :
      ℕ) =
    (↑((SimplexCategory.Hom.toOrderHom (𝟙 ⦋0⦌) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋0⦌.len + 1)) ⟨a, ha⟩) : ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
X Y : C
dsimp : Unique (Y ⟶ terminal.{v, u} C)
⊢ Unique (Y ⟶ Functor.obj.{w, v, w, u} (wideCospan ι X) none)

Tactic:
dsimp [wideCospan]

Premises used: CategoryTheory.CechNerveTerminalFrom.wideCospan
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ terminal.{v, u} C)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
        (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none ⟶
      Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none)
        (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (WidePullbackShape.Hom.id none))
        (Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          none
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) :
      Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    ((Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          none
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) ≫
        Functor.map (wideCospan ι X) (WidePullbackShape.Hom.id none) :
      Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
val : ι
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
        (some val) ⟶
      Functor.obj.{w, v, w, u} (wideCospan ι X) (some val))
    (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some val))
        (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (WidePullbackShape.Hom.id (some val)))
        (Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          (some val)
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some val) ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) (some val))
    ((Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          (some val)
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) ≫
        Functor.map (wideCospan ι X) (WidePullbackShape.Hom.id (some val)) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some val) ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) (some val))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
j : ι
term :
  Eq.{v + 1} (α := (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    (terminal.from (piObj.{w, v, u} fun (x : ι) ↦ X) : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ terminal.{v, u} C)
    (limit.π (Discrete.functor fun (x : ι) ↦ X) { as := j : Discrete ι } ≫
      Functor.map (wideCospan ι X) (WidePullbackShape.Hom.term j))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
        (some j) ⟶
      Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none)
        (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (WidePullbackShape.Hom.term j))
        (Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          none
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some j) ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    ((Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          (some j)
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) ≫
        Functor.map (wideCospan ι X) (WidePullbackShape.Hom.term j) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some j) ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, terminal.comp_from]

Premises used: CategoryTheory.Limits.terminal.comp_from, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
j : ι
⊢ Eq.{v + 1} (α := (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    (terminal.from (piObj.{w, v, u} fun (x : ι) ↦ X) : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ terminal.{v, u} C)
    (limit.π (Discrete.functor fun (x : ι) ↦ X) { as := j : Discrete ι } ≫
      Functor.map (wideCospan ι X) (WidePullbackShape.Hom.term j))

Tactic:
subsingleton