awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
f_1 : Arrow.{v, u} C
inst_1 :
  ∀ (n : ℕ), HasWidePushout.{0, v, u} f_1.left (fun (x : Fin (n + 1)) ↦ f_1.right) fun (x : Fin (n + 1)) ↦ f_1.hom
f g : Arrow.{v, u} C
inst_2 : ∀ (n : ℕ), HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
inst_3 : ∀ (n : ℕ), HasWidePushout.{0, v, u} g.left (fun (x : Fin (n + 1)) ↦ g.right) fun (x : Fin (n + 1)) ↦ g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (n.len + 1)
rw :
  Eq (α := f.left ⟶ g.cechConerve.obj n)
    (Hom.left F ≫
      g.hom ≫
        WidePushout.ι.{0, v, u} (C := C) (B := g.left) (objs := fun (i : Fin (n.len + 1)) ↦ g.right)
          (fun (x : Fin (n.len + 1)) ↦ g.hom) i)
    (Hom.left F ≫ WidePushout.head fun (x : Fin (n.len + 1)) ↦ g.hom)
rw₁ :
  Eq (α := f.left ⟶ g.cechConerve.obj n)
    (Hom.left F ≫
      g.hom ≫
        WidePushout.ι.{0, v, u} (C := C) (B := g.left) (objs := fun (i : Fin (n.len + 1)) ↦ g.right)
          (fun (x : Fin (n.len + 1)) ↦ g.hom) i)
    (Hom.left F ≫
      g.hom ≫
        WidePushout.ι.{0, v, u} (C := C) (B := g.left) (objs := fun (x : Fin (n.len + 1)) ↦ g.right)
          (fun (x : Fin (n.len + 1)) ↦ g.hom) i)
j : Fin (n.len + 1)
rw₂ :
  Eq (α := f.left ⟶ g.cechConerve.obj n)
    (Hom.left F ≫
      g.hom ≫
        WidePushout.ι.{0, v, u} (C := C) (B := g.left) (objs := fun (i : Fin (n.len + 1)) ↦ g.right)
          (fun (x : Fin (n.len + 1)) ↦ g.hom) i)
    (Hom.left F ≫
      g.hom ≫
        WidePushout.ι.{0, v, u} (C := C) (B := g.left) (objs := fun (x : Fin (n.len + 1)) ↦ g.right)
          (fun (x : Fin (n.len + 1)) ↦ g.hom) i)
j₁ : Fin (n.len + 1)
⊢ Eq (α := f.left ⟶ g.cechConerve.obj n)
    (f.hom ≫
      (fun (i : Fin (n.len + 1)) ↦
          (Hom.right F ≫
              WidePushout.ι.{0, v, u} (C := C) (B := g.left) (objs := fun (i : Fin (n.len + 1)) ↦ g.right)
                (fun (x : Fin (n.len + 1)) ↦ g.hom) i :
            f.right ⟶ g.cechConerve.obj n))
        i)
    (Hom.left F ≫ WidePushout.head fun (x : Fin (n.len + 1)) ↦ g.hom)

Tactic:
rw [← Arrow.w_assoc F, ← WidePushout.arrow_ι]

Premises used: CategoryTheory.Limits.WidePushout.arrow_ι, CategoryTheory.Arrow.w_assoc
-- 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
G : F.augmentedCechConerve ⟶ X
dsimp :
  Eq (α := F.left ⟶ X.right ^⦋0⦌) (G.left ≫ X.hom.app ⦋0⦌)
    (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 ≫
        G.right.app ⦋0⦌)
⊢ G.left ≫ (Functor.obj Augmented.toArrow X).hom =
    F.hom ≫
      WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (⦋0⦌.len + 1)) ↦ F.right)
          (fun (x : Fin (⦋0⦌.len + 1)) ↦ F.hom) 0 ≫
        G.right.app ⦋0⦌

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
G : F.augmentedCechConerve ⟶ X
rw :
  Eq (α := F.left ⟶ X.right ^⦋0⦌) (G.left ≫ X.hom.app ⦋0⦌)
    ((WidePushout.head fun (x : Fin 1) ↦ F.hom) ≫ G.right.app ⦋0⦌)
⊢ Eq (α := F.left ⟶ X.right ^⦋0⦌) (G.left ≫ X.hom.app ⦋0⦌)
    (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 ≫
        G.right.app ⦋0⦌)

Tactic:
rw [WidePushout.arrow_ι_assoc (fun (_ : Fin 1) => F.hom)]

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.Limits.WidePushout.arrow_ι_assoc
-- 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
G : F.augmentedCechConerve ⟶ X
⊢ Eq (α := F.left ⟶ X.right ^⦋0⦌) (G.left ≫ X.hom.app ⦋0⦌)
    ((WidePushout.head fun (x : Fin 1) ↦ F.hom) ≫ G.right.app ⦋0⦌)

Tactic:
congr_app G.w ⦋0⦌

Premises used: CategoryTheory.Functor.id, CategoryTheory.CommaMorphism.w, CategoryTheory.Limits.colimit, SimplexCategory.mk, CategoryTheory.Functor.const, CategoryTheory.Arrow, OfNat.ofNat, 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
G : F.augmentedCechConerve ⟶ X
⊢ Eq (α := F.left ⟶ X.right ^⦋0⦌) (G.left ≫ X.hom.app ⦋0⦌)
    ((WidePushout.head fun (x : Fin 1) ↦ F.hom) ≫ G.right.app ⦋0⦌)

Tactic:
exact congr_app G.w ⦋0⦌

Premises used: CategoryTheory.CommaMorphism.w, SimplexCategory.mk, OfNat.ofNat, 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
G : F ⟶ Functor.obj Augmented.toArrow X
x : SimplexCategory
j : Fin (x.len + 1)
rw :
  Arrow.Hom.left G ≫ (Functor.obj Augmented.toArrow X).hom ≫ X.right.map (⦋0⦌.const x j) =
    Arrow.Hom.left G ≫ X.hom.app x
⊢ F.hom ≫ (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) j =
    Arrow.Hom.left G ≫ X.hom.app x

Tactic:
rw [← Arrow.w_assoc G]

Premises used: CategoryTheory.Arrow.w_assoc
-- 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
G : F ⟶ Functor.obj Augmented.toArrow X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ Eq (α := Functor.obj (const C) X.left ^⦋0⦌ ⟶ (Functor.obj (𝟭 (CosimplicialObject.{v, u} C)) X.right).obj x)
    (Functor.map (Functor.obj (const C) X.left) (⦋0⦌.const x j) ≫ X.hom.app x)
    (X.hom.app ⦋0⦌ ≫ (Functor.obj (𝟭 (CosimplicialObject.{v, u} C)) X.right).map (⦋0⦌.const x j))

Tactic:
have t := X.hom.naturality (SimplexCategory.const ⦋0⦌ x j)
-- 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
G : F ⟶ Functor.obj Augmented.toArrow X
x : SimplexCategory
j : Fin (x.len + 1)
t :
  Eq (α := Functor.obj (const C) X.left ^⦋0⦌ ⟶ (Functor.obj (𝟭 (CosimplicialObject.{v, u} C)) X.right).obj x)
    (Functor.map (Functor.obj (const C) X.left) (⦋0⦌.const x j) ≫ X.hom.app x)
    (X.hom.app ⦋0⦌ ≫ (Functor.obj (𝟭 (CosimplicialObject.{v, u} C)) X.right).map (⦋0⦌.const x j))
dsimp :
  Arrow.Hom.left G ≫ CategoryStruct.comp (Y := X.right ^⦋0⦌) (X.hom.app ⦋0⦌) (X.right.map (⦋0⦌.const x j)) =
    Arrow.Hom.left G ≫ X.hom.app x
⊢ Arrow.Hom.left G ≫ (Functor.obj Augmented.toArrow X).hom ≫ X.right.map (⦋0⦌.const x j) =
    Arrow.Hom.left G ≫ X.hom.app x

Tactic:
dsimp at t ⊢
-- 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
G : F ⟶ Functor.obj Augmented.toArrow X
x : SimplexCategory
j : Fin (x.len + 1)
t : 𝟙 X.left ≫ X.hom.app x = CategoryStruct.comp (Y := X.right ^⦋0⦌) (X.hom.app ⦋0⦌) (X.right.map (⦋0⦌.const x j))
⊢ X.hom.app x = CategoryStruct.comp (Y := X.right ^⦋0⦌) (X.hom.app ⦋0⦌) (X.right.map (⦋0⦌.const x j))

Tactic:
simp only [Category.id_comp] at t

Premises used: CategoryTheory.Category.id_comp
-- 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
G : F ⟶ Functor.obj Augmented.toArrow X
x : SimplexCategory
j : Fin (x.len + 1)
t : X.hom.app x = CategoryStruct.comp (Y := X.right ^⦋0⦌) (X.hom.app ⦋0⦌) (X.right.map (⦋0⦌.const x j))
rw rw₁ : Arrow.Hom.left G ≫ X.hom.app x = Arrow.Hom.left G ≫ X.hom.app x
⊢ Arrow.Hom.left G ≫ CategoryStruct.comp (Y := X.right ^⦋0⦌) (X.hom.app ⦋0⦌) (X.right.map (⦋0⦌.const x j)) =
    Arrow.Hom.left G ≫ X.hom.app x

Tactic:
rw [← t]
-- 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
G : F ⟶ Functor.obj Augmented.toArrow X
x y : SimplexCategory
f : x ⟶ y
dsimp :
  Eq (α :=
    (widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom) ⟶
      X.right.obj y)
    (CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
      (WidePushout.desc (WidePushout.head fun (x : Fin (y.len + 1)) ↦ F.hom)
          (fun (i : Fin (x.len + 1)) ↦
            WidePushout.ι.{0, v, u} (J := Fin (y.len + 1)) (C := C) (B := F.left) (objs := fun (x : Fin (y.len + 1)) ↦
              F.right) (fun (x : Fin (y.len + 1)) ↦ F.hom)
              ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)))
          ⋯ :
        (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} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
      (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y)
          (fun (i : Fin (y.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ :
        (widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom) ⟶
          X.right.obj y))
    (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
      X.right.map f)
⊢ F.augmentedCechConerve.right.map f ≫
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y)
        (fun (i : Fin (y.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ =
    WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
      X.right.map f

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
G : F ⟶ Functor.obj Augmented.toArrow X
x y : SimplexCategory
f : x ⟶ y
j : Fin (x.len + 1)
a :
  Arrow.Hom.right G ≫
      X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) j)) =
    (Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j)) ≫ X.right.map f
⊢ 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)
      (CategoryStruct.comp (Y :=
        widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
        (WidePushout.desc (WidePushout.head fun (x : Fin (y.len + 1)) ↦ F.hom)
            (fun (i : Fin (x.len + 1)) ↦
              WidePushout.ι.{0, v, u} (J := Fin (y.len + 1)) (C := C) (B := F.left) (objs := fun (x : Fin (y.len + 1)) ↦
                F.right) (fun (x : Fin (y.len + 1)) ↦ F.hom)
                ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)))
            ⋯ :
          (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} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
        (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y)
            (fun (i : Fin (y.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ :
          (widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom) ⟶
            X.right.obj y)) =
    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 (Arrow.Hom.left G ≫ X.hom.app x)
          (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
        X.right.map f)

Tactic:
simp only [WidePushout.ι_desc_assoc, WidePushout.ι_desc]

Premises used: CategoryTheory.Limits.WidePushout.ι_desc_assoc, 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
G : F ⟶ Functor.obj Augmented.toArrow X
x y : SimplexCategory
f : x ⟶ y
j : Fin (x.len + 1)
a :
  Arrow.Hom.right G ≫
      X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) j)) =
    Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j ≫ f)
⊢ Arrow.Hom.right G ≫
      X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) j)) =
    (Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j)) ≫ X.right.map f

Tactic:
rw [Category.assoc, ← X.right.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comma.right, CategoryTheory.Functor.map_comp
-- 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
G : F ⟶ Functor.obj Augmented.toArrow X
x y : SimplexCategory
f : x ⟶ y
j : Fin (x.len + 1)
⊢ Arrow.Hom.right G ≫
      X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) j)) =
    Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j ≫ f)

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
G : F ⟶ Functor.obj Augmented.toArrow X
x y : SimplexCategory
f : x ⟶ y
⊢ 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)
      (CategoryStruct.comp (Y :=
        widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
        (WidePushout.desc (WidePushout.head fun (x : Fin (y.len + 1)) ↦ F.hom)
            (fun (i : Fin (x.len + 1)) ↦
              WidePushout.ι.{0, v, u} (J := Fin (y.len + 1)) (C := C) (B := F.left) (objs := fun (x : Fin (y.len + 1)) ↦
                F.right) (fun (x : Fin (y.len + 1)) ↦ F.hom)
                ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)))
            ⋯ :
          (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} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
        (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y)
            (fun (i : Fin (y.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ :
          (widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom) ⟶
            X.right.obj y)) =
    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 (Arrow.Hom.left G ≫ X.hom.app x)
          (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
        X.right.map f)

Tactic:
simp [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- 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
h₁ : CommaMorphism.left (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)) = A.left
h₂ :
  ∀ (x : SimplexCategory),
    NatTrans.app (CommaMorphism.right (equivalenceRightToLeft F X (equivalenceLeftToRight F X A))) x = A.right.app x
⊢ equivalenceRightToLeft F X (equivalenceLeftToRight F X A) = A

Tactic:
ext x : 2
-- 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
⊢ CommaMorphism.left (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)) = A.left

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
⊢ NatTrans.app (CommaMorphism.right (equivalenceRightToLeft F X (equivalenceLeftToRight F X A))) x = A.right.app x

Tactic:
WidePushout.hom_ext _ _ _ (fun j => ?_) ?_

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.WidePushout.hom_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.augmentedCechConerve ⟶ X
x : SimplexCategory
h₂ :
  ∀ (j : Fin (x.len + 1)),
    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 :
          F.right ⟶
            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.ι.{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
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 :
        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
⊢ NatTrans.app (CommaMorphism.right (equivalenceRightToLeft F X (equivalenceLeftToRight F X A))) x = A.right.app x

Tactic:
refine WidePushout.hom_ext _ _ _ (fun j => ?_) ?_

Premises used: CategoryTheory.Limits.WidePushout.hom_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.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
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.ι.{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
⊢ 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 :
        F.right ⟶ 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.ι.{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:
dsimp