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
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)
⊢ 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
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.ι.{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)))
      sorry) =
  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
-- 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
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)
      (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
have h₂ : WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
      (fun (x : Fin (x.len + 1)) ↦ F.hom)
      ((SimplexCategory.Hom.toOrderHom (⦋0⦌.const x j) : (a : Fin (0 + 1)) → Fin (x.len + 1)) 0) ≫
    A.right.app x =
  WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
      (fun (x : Fin (x.len + 1)) ↦ F.hom) j ≫
    A.right.app x
Tactic: simp only [Category.assoc, ← NatTrans.naturality A.right, Arrow.augmentedCechConerve_right,
          SimplexCategory.len_mk, Arrow.cechConerve_map, colimit.ι_desc,
          WidePushoutShape.mkCocone_ι_app, colimit.ι_desc_assoc]
-- 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
⊢ 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
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)
    (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)))
      sorry) =
  (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x
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
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom)
      (WidePushout.desc (A.left ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦
          CategoryStruct.comp (Y := X.right ^⦋0⦌)
            (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                (fun (x : Fin 1) ↦ F.hom) 0 ≫
              A.right.app ⦋0⦌)
            (X.right.map (⦋0⦌.const x i)))
        ⋯) =
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x
have h₂ : NatTrans.app
    (Cocone.ι
      (WidePushoutShape.mkCocone (A.left ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦
          CategoryStruct.comp (Y := X.right ^⦋0⦌)
            (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right)
                (fun (x : Fin 1) ↦ F.hom) 0 ≫
              A.right.app ⦋0⦌)
            (X.right.map (⦋0⦌.const x i)))
        sorry))
    none =
  (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom) ≫ A.right.app x
Tactic: rw [colimit.ι_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
A : F ⟶ Functor.obj Augmented.toArrow X
⊢ equivalenceLeftToRight F X (equivalenceRightToLeft F X A) = A
have h₁ : Arrow.Hom.left (equivalenceLeftToRight F X (equivalenceRightToLeft F X 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),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
h₁ : Arrow.Hom.left (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.left A
⊢ equivalenceLeftToRight F X (equivalenceRightToLeft F X A) = A
have h₂ : Arrow.Hom.right (equivalenceLeftToRight F X (equivalenceRightToLeft F X 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),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
A : F ⟶ Functor.obj Augmented.toArrow X
⊢ Arrow.Hom.right (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.right A
have h₂ : CategoryStruct.comp (Y := widePushout.{0, v, u} F.left (fun (x : Fin 1) ↦ F.right) fun (x : Fin 1) ↦ F.hom)
    (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right) (fun (x : Fin 1) ↦ F.hom) 0)
    (WidePushout.desc (Arrow.Hom.left A ≫ X.hom.app ⦋0⦌)
      (fun (i : Fin 1) ↦ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ i)) sorry) =
  Arrow.Hom.right A
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
A : F ⟶ Functor.obj Augmented.toArrow X
⊢ CategoryStruct.comp (Y := widePushout.{0, v, u} F.left (fun (x : Fin 1) ↦ F.right) fun (x : Fin 1) ↦ F.hom)
      (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin 1) ↦ F.right) (fun (x : Fin 1) ↦ F.hom) 0)
      (WidePushout.desc (Arrow.Hom.left A ≫ X.hom.app ⦋0⦌)
        (fun (i : Fin 1) ↦ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ i)) ⋯) =
    Arrow.Hom.right A
have h₂ : Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A
Tactic: rw [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
A : F ⟶ Functor.obj Augmented.toArrow X
⊢ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A
have h₂ : Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A ≫ 𝟙 (Functor.obj Augmented.toArrow X).right
Tactic: nth_rw 2 [← Category.comp_id A.right]
-- 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 ⟶ Functor.obj Augmented.toArrow X
⊢ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A ≫ 𝟙 (Functor.obj Augmented.toArrow X).right
have h₂ : X.right.map (⦋0⦌.const ⦋0⦌ 0) = 𝟙 (Functor.obj Augmented.toArrow X).right
Tactic: congr 1
-- 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 ⟶ Functor.obj Augmented.toArrow X
⊢ X.right.map (⦋0⦌.const ⦋0⦌ 0) = 𝟙 (Functor.obj Augmented.toArrow X).right
have h : ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌
Tactic: convert! X.right.map_id _
-- 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 ⟶ Functor.obj Augmented.toArrow X
⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌
have h : ∀ (a : ℕ) (ha : a < ⦋0⦌.len + 1),
  (↑((SimplexCategory.Hom.toOrderHom (⦋0⦌.const ⦋0⦌ 0) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋0⦌.len + 1))
          (⟨a, ha⟩ : Fin (⦋0⦌.len + 1))) :
      ℕ) =
    (↑((SimplexCategory.Hom.toOrderHom (𝟙 ⦋0⦌) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋0⦌.len + 1)) ⟨a, ha⟩) : ℕ)
Tactic: ext ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ Functor.obj.{w, v, w, u} (wideCospan ι X) none)
have dsimp : Unique (Y ⟶ terminal.{v, u} C)
Tactic: dsimp [wideCospan]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
j : ι
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
        (some j) ⟶
      Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none)
        (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (WidePullbackShape.Hom.term j))
        (Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          none
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some j) ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    ((Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          (some j)
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) ≫
        Functor.map (wideCospan ι X) (WidePullbackShape.Hom.term j) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some j) ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)
have term : Eq.{v + 1} (α := (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ Functor.obj.{w, v, w, u} (wideCospan ι X) none)
  (terminal.from (piObj.{w, v, u} fun (x : ι) ↦ X) : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ terminal.{v, u} C)
  (limit.π (Discrete.functor fun (x : ι) ↦ X) { as := j : Discrete ι } ≫
    Functor.map (wideCospan ι X) (WidePullbackShape.Hom.term j))
Tactic: simp only [Functor.const_obj_obj, Functor.const_obj_map, terminal.comp_from]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
⊢ f = Pi.lift fun (j : ι) ↦ s.π.app (some j)
have h₁ : ∀ (j : ι),
  f ≫ Pi.π (fun (x : ι) ↦ X) j =
    CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X) (Pi.lift fun (j : ι) ↦ s.π.app (some j))
      (Pi.π (fun (x : ι) ↦ X) j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j =
    CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X) (Pi.lift fun (j : ι) ↦ s.π.app (some j))
      (Pi.π (fun (x : ι) ↦ X) j)
have h₁ : f ≫ Pi.π (fun (x : ι) ↦ X) j =
  CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
    (limit.lift (Discrete.functor fun (x : ι) ↦ X) (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j)))
    (Pi.π (fun (x : ι) ↦ X) j)
Tactic: dsimp only [Limits.Pi.lift]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j =
    CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
      (limit.lift (Discrete.functor fun (x : ι) ↦ X) (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j)))
      (Pi.π (fun (x : ι) ↦ X) j)
have h₁ : f ≫ Pi.π (fun (x : ι) ↦ X) j = NatTrans.app (Cone.π (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j))) { as := j }
Tactic: rw [limit.lift_π]