awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq (α :=
    (HomologicalComplex.X (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1)).X ⟶
      (HomologicalComplex.X (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) n).X)
    (Karoubi.Hom.f
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n))
    (P.p.app (op ⦋n + 1⦌) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
have dsimp : Eq (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
  (Karoubi.Hom.f
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n) :
    KaroubiFunctorCategoryEmbedding.obj P _⦋n + 1⦌.X ⟶ KaroubiFunctorCategoryEmbedding.obj P _⦋n⦌.X)
  (P.p.app (op ⦋n + 1⦌) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (Karoubi.Hom.f
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n) :
      KaroubiFunctorCategoryEmbedding.obj P _⦋n + 1⦌.X ⟶ KaroubiFunctorCategoryEmbedding.obj P _⦋n⦌.X)
    (P.p.app (op ⦋n + 1⦌) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
have simp : Eq.{v_1 + 1} (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
  (∑ x : Fin (n + 2),
    HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f)
  (∑ x : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • P.p.app (op ⦋n + 1⦌) ≫ P.X.δ x)
Tactic: simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum,
    Karoubi.zsmul_hom, Preadditive.comp_zsmul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
⊢ Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
    (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X)
    (Functor.obj (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) X)
have refine : { f :
  HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
    Functor.obj SimplicialObject.Augmented.point X //
  Eq (α :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
      Functor.obj SimplicialObject.Augmented.point X)
    (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0 ≫ f) 0 }
Tactic: refine (ChainComplex.toSingle₀Equiv _ _).symm ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
⊢ { f :
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
      Functor.obj SimplicialObject.Augmented.point X //
    Eq (α :=
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
        Functor.obj SimplicialObject.Augmented.point X)
      (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0 ≫ f) 0 }
have refine : Eq (α :=
  HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
    Functor.obj SimplicialObject.Augmented.point X)
  (CategoryStruct.comp (Y :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0)
    (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0)
    (X.hom.app (op ⦋0⦌)))
  0
Tactic: refine ⟨X.hom.app (op ⦋0⦌), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
      Functor.obj SimplicialObject.Augmented.point X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0)
      (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0)
      (X.hom.app (op ⦋0⦌)))
    0
have dsimp : Eq (α := X.left _⦋1⦌ ⟶ X.right)
  (CategoryStruct.comp (Y := X.left _⦋0⦌) (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X.left) 1 0)
      (X.hom.app (op ⦋0⦌)) :
    X.left _⦋1⦌ ⟶ X.right)
  (0 :
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
      Functor.obj SimplicialObject.Augmented.point X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : SimplicialObject.Augmented.{v_1, u_1} C
⊢ Eq (α := X.left _⦋1⦌ ⟶ X.right)
    (CategoryStruct.comp (Y := X.left _⦋0⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X.left) 1 0) (X.hom.app (op ⦋0⦌)) :
      X.left _⦋1⦌ ⟶ X.right)
    (0 :
      HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
        Functor.obj SimplicialObject.Augmented.point X)
have rw : HAdd.hAdd (α := X.left _⦋1⦌ ⟶ X.right)
    (X.hom.app (op ⦋HAdd.hAdd (α := ℕ) 0 1⦌) ≫ SimplicialObject.δ (Functor.obj (SimplicialObject.const C) X.right) 0)
    (-X.hom.app (op ⦋HAdd.hAdd (α := ℕ) 0 1⦌) ≫ SimplicialObject.δ (Functor.obj (SimplicialObject.const C) X.right) 1) =
  0
Tactic: rw [alternatingFaceMapComplex_obj_d, objD, Fin.sum_univ_two, Fin.val_zero,
      pow_zero, one_smul, Fin.val_one, pow_one, neg_smul, one_smul, add_comp,
      neg_comp, SimplicialObject.δ_naturality, SimplicialObject.δ_naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : CosimplicialObject.{v_1, u_1} C
n : ℕ
⊢ objD X n =
    (AlternatingFaceMapComplex.objD (Functor.obj (Equivalence.functor (cosimplicialSimplicialEquiv C)) (op X)) n).unop
have simp : Eq.{v_1 + 1} (α := X ^⦋n⦌ ⟶ X ^⦋n + 1⦌) (∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i)
  (∑ x : Fin (n + 2),
    HPow.hPow (α := ℤ) (-1) (↑x : ℕ) •
      ((Functor.obj (Equivalence.functor (cosimplicialSimplicialEquiv C)) (op X)).δ x).unop)
Tactic: simp only [objD, AlternatingFaceMapComplex.objD, unop_sum, unop_zsmul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq (α := HomologicalComplex.X (obj X) n ⟶ HomologicalComplex.X (obj Y) (n + 1))
    ((fun (n : ℕ) ↦ (f.app ⦋n⦌ : X ^⦋n⦌ ⟶ Y ^⦋n⦌)) n ≫ HomologicalComplex.d (obj Y) n (n + 1))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) (n + 1)) (HomologicalComplex.d (obj X) n (n + 1))
      ((fun (n : ℕ) ↦ (f.app ⦋n⦌ : X ^⦋n⦌ ⟶ Y ^⦋n⦌)) (n + 1)))
have simp : Eq (α := X ^⦋n⦌ ⟶ Y ^⦋n + 1⦌) (f.app ⦋n⦌ ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • Y.δ i)
  ((∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ f.app ⦋n + 1⦌)
Tactic: simp only [obj, CochainComplex.of_d, objD, Int.reduceNeg]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq (α := X ^⦋n⦌ ⟶ Y ^⦋n + 1⦌) (f.app ⦋n⦌ ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • Y.δ i)
    ((∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ f.app ⦋n + 1⦌)
have rw : Eq.{v_1 + 1} (α := X ^⦋n⦌ ⟶ Y ^⦋n + 1⦌) (∑ j : Fin (n + 2), f.app ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
  (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app ⦋n + 1⦌)
Tactic: rw [comp_sum, sum_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq.{v_1 + 1} (α := X ^⦋n⦌ ⟶ Y ^⦋n + 1⦌) (∑ j : Fin (n + 2), f.app ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • Y.δ j))
    (∑ j : Fin (n + 2), (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ f.app ⦋n + 1⦌)
have refine : ∀ (x : Fin (n + 2)),
  Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x →
    f.app ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) = (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app ⦋n + 1⦌
Tactic: refine Finset.sum_congr rfl fun x _ => ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
⊢ f.app ⦋n⦌ ≫ (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • Y.δ x) = (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x) ≫ f.app ⦋n + 1⦌
have rw : HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • f.app ⦋n⦌ ≫ Y.δ x = HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app ⦋n + 1⦌
Tactic: rw [comp_zsmul, zsmul_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
⊢ HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • f.app ⦋n⦌ ≫ Y.δ x = HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • X.δ x ≫ f.app ⦋n + 1⦌
have e_a : f.app ⦋n⦌ ≫ Y.δ x = X.δ x ≫ f.app ⦋n + 1⦌
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
X Y : CosimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
h : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ x
⊢ f.app ⦋n⦌ ≫ Y.δ x = X.δ x ≫ f.app ⦋n + 1⦌
have e_a : X.δ x ≫ f.app ⦋n + 1⦌ = f.app ⦋n⦌ ≫ Y.δ x
Tactic: symm
-- 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),
    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
⊢ 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
have this : Functor.map (𝟭 (SimplicialObject.{v, u} C)) G.left ≫ F.augmentedCechNerve.hom = X.hom ≫ Functor.map (const C) G.right
Tactic: have := G.w
-- 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),
    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
⊢ 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
have 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⦌))
Tactic: apply_fun fun e => e.app (Opposite.op ⦋0⦌) at this
Cleared hypotheses: this
-- 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),
    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
⊢ 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
have 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)
      sorry)
  (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)
        sorry :
      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))
        sorry :
      (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))
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),
    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)
⊢ 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)
have 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
Tactic: simp only [WidePullback.lift_π, Category.assoc, ← X.left.map_comp_assoc]
-- 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),
    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
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F A) = A
have h₁ : Arrow.Hom.left (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.left A
Tactic: ext
-- 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),
    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
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F A) = A
have h₂ : Arrow.Hom.right (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.right A
Tactic: ext
-- 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),
    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
⊢ equivalenceLeftToRight X F (equivalenceRightToLeft X F A) = A
have h₁ : ∀ (x : SimplexCategoryᵒᵖ),
  NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x = A.left.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),
    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
⊢ equivalenceLeftToRight X F (equivalenceRightToLeft X F A) = A
have h₂ : CommaMorphism.right (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)) = A.right
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),
    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
have 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
Tactic: refine WidePullback.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),
    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
⊢ NatTrans.app (CommaMorphism.left (equivalenceLeftToRight X F (equivalenceRightToLeft X F A))) x = A.left.app x
have 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
Tactic: refine WidePullback.hom_ext _ _ _ (fun j => ?_) ?_