awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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
⊢ (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
have 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)
Tactic: refine WidePushout.desc (WidePushout.head _)
      (fun i => (@WidePushout.ι _ _ _ _ _ (fun _ => f.hom) (_) (g.toOrderHom i))) (fun j => ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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)
⊢ 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)
have 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)))
Tactic: rw [← WidePushout.arrow_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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)))
⊢ 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)
have j₁ : Fin (y.len + 1)
Tactic: rw [← WidePushout.arrow_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← Arrow.w_assoc F, ← WidePushout.arrow_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← Arrow.w_assoc F, ← WidePushout.arrow_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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
⊢ 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⦌
have 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⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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⦌)
    (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⦌)
have 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⦌)
Tactic: rw [WidePushout.arrow_ι_assoc (fun (_ : Fin 1) => F.hom)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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)
⊢ 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
have 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
Tactic: rw [← Arrow.w_assoc G]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (hypothesis)
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)
⊢ 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
have 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))
Tactic: have t := X.hom.naturality (SimplexCategory.const ⦋0⦌ x j)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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))
⊢ 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
have 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
Tactic: dsimp at t ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (hypothesis)
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))
⊢ 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
have t₁ : 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
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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))
⊢ 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
have rw : Arrow.Hom.left G ≫ X.hom.app x = Arrow.Hom.left G ≫ X.hom.app x
Tactic: rw [← t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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
⊢ 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
have 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)))
        sorry :
      (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)) sorry :
      (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)) sorry ≫
    X.right.map f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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)
⊢ 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)
have 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
Tactic: simp only [WidePushout.ι_desc_assoc, WidePushout.ι_desc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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)) ≫ X.right.map f
have 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)
Tactic: rw [Category.assoc, ← X.right.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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
⊢ equivalenceRightToLeft F X (equivalenceLeftToRight F X A) = A
have h₁ : CommaMorphism.left (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)) = A.left
Tactic: ext x : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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
⊢ equivalenceRightToLeft F X (equivalenceLeftToRight F X A) = A
have h₂ : ∀ (x : SimplexCategory),
  NatTrans.app (CommaMorphism.right (equivalenceRightToLeft F X (equivalenceLeftToRight F X A))) x = A.right.app x
Tactic: ext x : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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
have 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
Tactic: refine WidePushout.hom_ext _ _ _ (fun j => ?_) ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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
⊢ NatTrans.app (CommaMorphism.right (equivalenceRightToLeft F X (equivalenceLeftToRight F X A))) x = A.right.app x
have 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
Tactic: refine WidePushout.hom_ext _ _ _ (fun j => ?_) ?_