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),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : X ⟶ F.augmentedCechNerve
this :
  Functor.map (𝟭 (SimplicialObject.{v, u} C)) G.left ≫ F.augmentedCechNerve.hom = X.hom ≫ Functor.map (const C) G.right
⊢ Eq (α :=
    Functor.obj (𝟭 (SimplicialObject.{v, u} C)) X.left _⦋0⦌ ⟶ Functor.obj (const C) F.augmentedCechNerve.right _⦋0⦌)
    ((Functor.map (𝟭 (SimplicialObject.{v, u} C)) G.left ≫ F.augmentedCechNerve.hom).app (Opposite.op ⦋0⦌))
    ((X.hom ≫ Functor.map (const C) G.right).app (Opposite.op ⦋0⦌))

Tactic:
apply_fun fun e => e.app (Opposite.op ⦋0⦌) at this
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : X ⟶ F.augmentedCechNerve
this :
  Eq (α :=
    Functor.obj (𝟭 (SimplicialObject.{v, u} C)) X.left _⦋0⦌ ⟶ Functor.obj (const C) F.augmentedCechNerve.right _⦋0⦌)
    ((Functor.map (𝟭 (SimplicialObject.{v, u} C)) G.left ≫ F.augmentedCechNerve.hom).app (Opposite.op ⦋0⦌))
    ((X.hom ≫ Functor.map (const C) G.right).app (Opposite.op ⦋0⦌))
⊢ Functor.map (𝟭 C)
        (G.left.app (Opposite.op ⦋0⦌) ≫
          WidePullback.π (fun (x : Fin ((Opposite.unop (Opposite.op ⦋0⦌)).len + 1)) ↦ F.hom) 0) ≫
      F.hom =
    (Functor.obj Augmented.toArrow X).hom ≫ Functor.map (𝟭 C) G.right

Tactic:
simpa using this
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : Functor.obj Augmented.toArrow X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin ((Opposite.unop x).len + 1)
⊢ (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
          X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
        i ≫
      F.hom =
    X.hom.app x ≫ Arrow.Hom.right G

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : Functor.obj Augmented.toArrow X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
dsimp :
  Eq (α :=
    X.left.obj x ⟶
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
    (X.left.map f ≫
      WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
        (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
          X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) i)) ≫ Arrow.Hom.left G)
        ⋯)
    (CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
            X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
          ⋯ :
        X.left.obj x ⟶
          widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (WidePullback.lift (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
          (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
            WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
              ((SimplexCategory.Hom.toOrderHom f.unop :
                  (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
                i))
          ⋯ :
        (widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) ⟶
          widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom))
⊢ X.left.map f ≫
      WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
        (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
          X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) i)) ≫ Arrow.Hom.left G)
        ⋯ =
    WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
        (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
          X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
        ⋯ ≫
      F.augmentedCechNerve.left.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),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : Functor.obj Augmented.toArrow X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j : Fin ((Opposite.unop y).len + 1)
a :
  X.left.map (f ≫ Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) j)) ≫ Arrow.Hom.left G =
    X.left.map
        (Quiver.Hom.op
          (⦋0⦌.const (Opposite.unop x)
            ((SimplexCategory.Hom.toOrderHom f.unop :
                (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
              j))) ≫
      Arrow.Hom.left G
⊢ CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
      (X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
            X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) i)) ≫ Arrow.Hom.left G)
          ⋯)
      (WidePullback.π (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom) j) =
    CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
      (CategoryStruct.comp (Y :=
        widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
          fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
        (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
            (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
              X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
            ⋯ :
          X.left.obj x ⟶
            widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
              fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
        (WidePullback.lift (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
            (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
              WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
                ((SimplexCategory.Hom.toOrderHom f.unop :
                    (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
                  i))
            ⋯ :
          (widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
              fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) ⟶
            widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
              fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom))
      (WidePullback.π (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom) j)

Tactic:
simp only [WidePullback.lift_π, Category.assoc, ← X.left.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comma.left, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Limits.WidePullback.lift_π
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : Functor.obj Augmented.toArrow X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j : Fin ((Opposite.unop y).len + 1)
⊢ X.left.map (f ≫ Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) j)) ≫ Arrow.Hom.left G =
    X.left.map
        (Quiver.Hom.op
          (⦋0⦌.const (Opposite.unop x)
            ((SimplexCategory.Hom.toOrderHom f.unop :
                (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
              j))) ≫
      Arrow.Hom.left G

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : Functor.obj Augmented.toArrow X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
      (X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
            X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) i)) ≫ Arrow.Hom.left G)
          ⋯)
      (WidePullback.base fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom) =
    CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
      (CategoryStruct.comp (Y :=
        widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
          fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
        (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
            (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
              X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
            ⋯ :
          X.left.obj x ⟶
            widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
              fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
        (WidePullback.lift (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
            (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
              WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
                ((SimplexCategory.Hom.toOrderHom f.unop :
                    (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
                  i))
            ⋯ :
          (widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
              fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) ⟶
            widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
              fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom))
      (WidePullback.base fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
A : Functor.obj Augmented.toArrow X ⟶ F
h₁ : Arrow.Hom.left (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.left A
h₂ : Arrow.Hom.right (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.right A
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F 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),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
A : Functor.obj Augmented.toArrow X ⟶ F
⊢ Arrow.Hom.left (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.left A

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

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
A : X ⟶ F.augmentedCechNerve
h₁ :
  ∀ (x : SimplexCategoryᵒᵖ),
    NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x = A.left.app x
h₂ : CommaMorphism.right (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)) = A.right
⊢ equivalenceLeftToRight X F (equivalenceRightToLeft X F 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),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x = A.left.app x

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

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.WidePullback.hom_ext
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
h₁ :
  ∀ (j : Fin ((Opposite.unop x).len + 1)),
    CategoryStruct.comp (Y :=
        widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
          fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
        (NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x :
          X.left.obj x ⟶ F.augmentedCechNerve.left.obj x)
        (WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) j) =
      A.left.app x ≫ WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) j
h₂ :
  CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x :
        X.left.obj x ⟶ F.augmentedCechNerve.left.obj x)
      (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) =
    A.left.app x ≫ WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom
⊢ NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x = A.left.app x

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

Premises used: CategoryTheory.Limits.WidePullback.hom_ext
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
j : Fin ((Opposite.unop x).len + 1)
⊢ CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x :
        X.left.obj x ⟶ F.augmentedCechNerve.left.obj x)
      (WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) j) =
    A.left.app x ≫ WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x :
        X.left.obj x ⟶ F.augmentedCechNerve.left.obj x)
      (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) =
    A.left.app x ≫ WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom

Tactic:
simpa using congr_app A.w.symm x

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

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
f : Arrow.{v, u} C
inst_1 : ∀ (n : ℕ), HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
x y : SimplexCategory
g : x ⟶ y
refine :
  ∀ (j : Fin (x.len + 1)),
    Eq (α :=
      f.left ⟶ widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom)
      (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 g : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)) :
              f.right ⟶
                widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom))
          j)
      (WidePushout.head fun (x : Fin (y.len + 1)) ↦ f.hom)
⊢ (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

Tactic:
refine WidePushout.desc (WidePushout.head _)
      (fun i => (@WidePushout.ι _ _ _ _ _ (fun _ => f.hom) (_) (g.toOrderHom i))) (fun j => ?_)

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.Limits.WidePushout.head, CategoryTheory.Limits.WidePushout.ι, SimplexCategory.Hom.toOrderHom, CategoryTheory.Limits.WidePushout.desc, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
f : Arrow.{v, u} C
inst_1 : ∀ (n : ℕ), HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
x y : SimplexCategory
g : x ⟶ y
j : Fin (x.len + 1)
rw :
  Eq (α :=
    f.left ⟶ widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom)
    (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 g : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)) :
            f.right ⟶
              widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom))
        j)
    (f.hom ≫
      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 g : (a : Fin (x.len + 1)) → Fin (y.len + 1)) j : Fin (y.len + 1)))
j₁ : Fin (y.len + 1)
rw₁ :
  Eq (α :=
    f.left ⟶ widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom)
    (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 g : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)) :
            f.right ⟶
              widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom))
        j)
    (f.hom ≫
      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 g : (a : Fin (x.len + 1)) → Fin (y.len + 1)) j : Fin (y.len + 1)))
j₂ : Fin (y.len + 1)
⊢ Eq (α :=
    f.left ⟶ widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom)
    (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 g : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)) :
            f.right ⟶
              widePushout.{0, v, u} f.left (fun (x : Fin (y.len + 1)) ↦ f.right) fun (x : Fin (y.len + 1)) ↦ f.hom))
        j)
    (WidePushout.head fun (x : Fin (y.len + 1)) ↦ f.hom)

Tactic:
rw [← WidePushout.arrow_ι]

Premises used: CategoryTheory.Limits.WidePushout.arrow_ι
-- 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)
⊢ g.right ⟶ g.cechConerve.obj n

Tactic:
apply WidePushout.ι _ i

Premises used: CategoryTheory.Limits.WidePushout.ι