awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
pb : (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i : X.I × Y.I).1 ≫ eqToHom ⋯) (g.φ (↑i : X.I × Y.I).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct.{w, u} C
s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }
⊢ (fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
        (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
            (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) ⋯ :
          { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
      ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
          ({
              f := fun (i : T.I) ↦
                Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                  ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯,
              φ := fun (i : T.I) ↦
                IsLimit.lift
                  (hpb
                    ((fun (i : T.I) ↦
                        (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                            ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯ :
                          { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                      i))
                  (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i) ⋯) } :
            Hom.{w, v, u} T (pullbackCone f g pb).pt))
        s) =
    s
have a : ∀ (x : T.I),
  Hom.f.{w, v, u}
      (↑((fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
                (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
                    (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) sorry :
                  { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
              ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
                  ({
                      f := fun (i : T.I) ↦
                        Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                          ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) sorry,
                      φ := fun (i : T.I) ↦
                        IsLimit.lift
                          (hpb
                            ((fun (i : T.I) ↦
                                (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                                    ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) sorry :
                                  { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                              i))
                          (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i) sorry) } :
                    Hom.{w, v, u} T (pullbackCone f g pb).pt))
                s)) :
          (T ⟶ X) × (T ⟶ Y)).1
      x =
    (↑s : (T ⟶ X) × (T ⟶ Y)).1.f x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
pb : (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i : X.I × Y.I).1 ≫ eqToHom ⋯) (g.φ (↑i : X.I × Y.I).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct.{w, u} C
⊢ IsLimit (pullbackCone f g pb)
have refine : ∀ (s : PullbackCone f g) (m : s.pt ⟶ (pullbackCone f g pb).pt) (h₁ : m ≫ (pullbackCone f g pb).fst = s.fst)
  (h₂ : m ≫ (pullbackCone f g pb).snd = s.snd),
  m =
    (fun (s : PullbackCone f g) ↦
        Equiv.invFun (homPullbackEquiv f g pb hpb s.pt)
          (Subtype.mk (p := fun (p : (s.pt ⟶ X) × (s.pt ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g) (s.fst, s.snd) sorry))
      s
Tactic: refine PullbackCone.IsLimit.mk
    (fst := (pullbackCone f g pb).fst) (snd := (pullbackCone f g pb).snd) _
    (fun s ↦ (homPullbackEquiv f g pb hpb s.pt).2 ⟨(s.fst, s.snd), s.condition⟩)
    (fun s ↦ congrArg (·.1.fst)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s ↦ congrArg (·.1.snd)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s m h₁ h₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
pb : (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i : X.I × Y.I).1 ≫ eqToHom ⋯) (g.φ (↑i : X.I × Y.I).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct.{w, u} C
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ m =
    (fun (s : PullbackCone f g) ↦
        Equiv.invFun (homPullbackEquiv f g pb hpb s.pt)
          (Subtype.mk (p := fun (p : (s.pt ⟶ X) × (s.pt ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g) (s.fst, s.snd) ⋯))
      s
have h : (s.fst, s.snd) =
  (↑((homPullbackEquiv f g pb hpb s.pt :
            (s.pt ⟶ (pullbackCone f g pb).pt) ≃ { p : (s.pt ⟶ X) × (s.pt ⟶ Y) // p.1 ≫ f = p.2 ≫ g }).1
        m) :
    (s.pt ⟶ X) × (s.pt ⟶ Y))
Tactic: convert! ((homPullbackEquiv f g pb hpb s.pt).left_inv m).symm using 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
pb : (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i : X.I × Y.I).1 ≫ eqToHom ⋯) (g.φ (↑i : X.I × Y.I).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct.{w, u} C
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ (s.fst, s.snd) =
    (↑((homPullbackEquiv f g pb hpb s.pt :
              (s.pt ⟶ (pullbackCone f g pb).pt) ≃ { p : (s.pt ⟶ X) × (s.pt ⟶ Y) // p.1 ≫ f = p.2 ≫ g }).1
          m) :
      (s.pt ⟶ X) × (s.pt ⟶ Y))
have h : (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) =
  (↑((homPullbackEquiv f g pb hpb s.pt :
            (s.pt ⟶ (pullbackCone f g pb).pt) ≃ { p : (s.pt ⟶ X) × (s.pt ⟶ Y) // p.1 ≫ f = p.2 ≫ g }).1
        m) :
    (s.pt ⟶ X) × (s.pt ⟶ Y))
Tactic: rw [← h₁, ← h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
x : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
x_1 : α
⊢ CategoryStruct.comp (Y := Cone.pt (U.powerFan α))
      ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
          ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
              φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
            Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
        x)
      (Fan.proj (U.powerFan α) x_1) =
    x.proj x_1
have h₁ : ∀ (x_2 : x.pt.I),
  Hom.f.{w, v, u}
      (CategoryStruct.comp (Y := Cone.pt (U.powerFan α))
        ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
            ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
                φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
              Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
          x)
        (Fan.proj (U.powerFan α) x_1))
      x_2 =
    (x.proj x_1).f x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
x : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
x_1 : α
h₁ :
  ∀ (x_2 : x.pt.I),
    Hom.f.{w, v, u}
        (CategoryStruct.comp (Y := Cone.pt (U.powerFan α))
          ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
              ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
                  φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
                Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
            x)
          (Fan.proj (U.powerFan α) x_1))
        x_2 =
      (x.proj x_1).f x_2
⊢ CategoryStruct.comp (Y := Cone.pt (U.powerFan α))
      ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
          ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
              φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
            Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
        x)
      (Fan.proj (U.powerFan α) x_1) =
    x.proj x_1
have h₂ : ∀ (i : x.pt.I),
  CategoryStruct.comp (Y :=
      U.obj
        (Hom.f.{w, v, u}
          (CategoryStruct.comp (Y := Cone.pt (U.powerFan α))
            ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
                ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
                    φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
                  Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
              x)
            (Fan.proj (U.powerFan α) x_1))
          i))
      (Hom.φ
        (CategoryStruct.comp (Y := Cone.pt (U.powerFan α))
          ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
              ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
                  φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
                Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
            x)
          (Fan.proj (U.powerFan α) x_1))
        i)
      (eqToHom sorry) =
    (x.proj x_1).φ i
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
m : s.pt ⟶ Cone.pt (U.powerFan α)
hm : ∀ (j : α), m ≫ Fan.proj (U.powerFan α) j = s.proj j
⊢ m =
    (fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
        ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
            φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
          Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
      s
have obtain : ∀ (f : s.pt.I → (Cone.pt (U.powerFan α)).I) (φ : (i : s.pt.I) → s.pt.obj i ⟶ (Cone.pt (U.powerFan α)).obj (f i))
  (hm :
    ∀ (j : α), { f := f, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫ Fan.proj (U.powerFan α) j = s.proj j),
  { f := f, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } =
    (fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
        ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
            φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
          Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
      s
Tactic: obtain ⟨f, φ⟩ := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
f : s.pt.I → (Cone.pt (U.powerFan α)).I
φ : (i : s.pt.I) → s.pt.obj i ⟶ (Cone.pt (U.powerFan α)).obj (f i)
hm : ∀ (j : α), { f := f, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫ Fan.proj (U.powerFan α) j = s.proj j
⊢ f = fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i
have h : ∀ (i : s.pt.I), f i = fun (a : α) ↦ (s.proj a).f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
f : s.pt.I → (Cone.pt (U.powerFan α)).I
φ : (i : s.pt.I) → s.pt.obj i ⟶ (Cone.pt (U.powerFan α)).obj (f i)
hm : ∀ (j : α), { f := f, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫ Fan.proj (U.powerFan α) j = s.proj j
i : s.pt.I
⊢ f i = fun (a : α) ↦ (s.proj a).f i
have h : ∀ (a : α), f i a = (s.proj a).f i
Tactic: ext a
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
f : s.pt.I → (Cone.pt (U.powerFan α)).I
φ : (i : s.pt.I) → s.pt.obj i ⟶ (Cone.pt (U.powerFan α)).obj (f i)
hm : ∀ (j : α), { f := f, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫ Fan.proj (U.powerFan α) j = s.proj j
⊢ { f := f, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } =
    (fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
        ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
            φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
          Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
      s
have obtain : ∀ (φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i))
  (hm :
    ∀ (j : α),
      { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
          Fan.proj (U.powerFan α) j =
        s.proj j),
  { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } =
    (fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
        ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
            φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
          Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
      s
Tactic: obtain rfl : f = fun i a ↦ (s.proj a).f i := by
        ext i
        dsimp
        ext a
        exact congr_fun (congr_arg FormalCoproduct.Hom.f (hm a)) i
Cleared hypotheses: f, φ, hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i)
hm :
  ∀ (j : α),
    { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
        Fan.proj (U.powerFan α) j =
      s.proj j
⊢ { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } =
    (fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
        ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
            φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
          Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
      s
have h₁ : ∀ (i : s.pt.I),
  { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) }.f i =
    Hom.f.{w, v, u}
      ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
          ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
              φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
            Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
        s)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i)
hm :
  ∀ (j : α),
    { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
        Fan.proj (U.powerFan α) j =
      s.proj j
h₁ :
  ∀ (i : s.pt.I),
    { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) }.f i =
      Hom.f.{w, v, u}
        ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
            ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
                φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
              Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
          s)
        i
⊢ { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } =
    (fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
        ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
            φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
          Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
      s
have h₂ : ∀ (i : s.pt.I),
  Eq (α :=
    s.pt.obj i ⟶
      (Cone.pt (U.powerFan α)).obj
        (Hom.f.{w, v, u}
          ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
              ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
                  φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
                Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
            s)
          i))
    ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) }.φ i ≫
      eqToHom sorry)
    (Hom.φ
      ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
          ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
              φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
            Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
        s)
      i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i)
hm :
  ∀ (j : α),
    { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
        Fan.proj (U.powerFan α) j =
      s.proj j
i : s.pt.I
⊢ Eq (α :=
    s.pt.obj i ⟶
      (Cone.pt (U.powerFan α)).obj
        (Hom.f.{w, v, u}
          ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
              ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
                  φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
                Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
            s)
          i))
    ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) }.φ i ≫
      eqToHom ⋯)
    (Hom.φ
      ((fun (s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U) ↦
          ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i,
              φ := fun (i : s.pt.I) ↦ Pi.lift fun (a : α) ↦ (s.proj a).φ i } :
            Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α))))
        s)
      i)
have h₂ : φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i)) = Pi.lift fun (a : α) ↦ (s.proj a).φ i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i)
hm :
  ∀ (j : α),
    { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
        Fan.proj (U.powerFan α) j =
      s.proj j
i : s.pt.I
⊢ φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i)) = Pi.lift fun (a : α) ↦ (s.proj a).φ i
have h₂ : ∀ (a : α),
  (φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))) ≫
      Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a =
    CategoryStruct.comp (Y := piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))
      (Pi.lift fun (a : α) ↦ (s.proj a).φ i) (Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a)
Tactic: ext a
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i)
hm :
  ∀ (j : α),
    { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
        Fan.proj (U.powerFan α) j =
      s.proj j
i : s.pt.I
a : α
⊢ (φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))) ≫
      Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a =
    CategoryStruct.comp (Y := piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))
      (Pi.lift fun (a : α) ↦ (s.proj a).φ i) (Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a)
have hm₁ : { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
    Fan.proj (U.powerFan α) a =
  s.proj a
Tactic: specialize hm a
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i)
i : s.pt.I
a : α
hm :
  { f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
      Fan.proj (U.powerFan α) a =
    s.proj a
⊢ (φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))) ≫
      Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a =
    CategoryStruct.comp (Y := piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))
      (Pi.lift fun (a : α) ↦ (s.proj a).φ i) (Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a)
have hm₁ : ∃ (h₁ :
  Hom.f.{w, v, u}
      ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
        Fan.proj (U.powerFan α) a) =
    (s.proj a).f),
  ∀ (i : s.pt.I),
    Hom.φ
          ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
            Fan.proj (U.powerFan α) a)
          i ≫
        eqToHom sorry =
      (s.proj a).φ i
Tactic: rw [hom_ext_iff] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
U : FormalCoproduct.{w, u} C
α : Type
inst_1 : HasProductsOfShape.{0, u, v} α C
s : Fan (C := FormalCoproduct.{w, u} C) fun (x : α) ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ obj.{w, u} (Cone.pt (U.powerFan α)) ((fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i) i)
i : s.pt.I
a : α
hm :
  ∃ (h₁ :
    Hom.f.{w, v, u}
        ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
          Fan.proj (U.powerFan α) a) =
      (s.proj a).f),
    ∀ (i : s.pt.I),
      Hom.φ
            ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
              Fan.proj (U.powerFan α) a)
            i ≫
          eqToHom ⋯ =
        (s.proj a).φ i
⊢ (φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))) ≫
      Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a =
    CategoryStruct.comp (Y := piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i))
      (Pi.lift fun (a : α) ↦ (s.proj a).φ i) (Pi.π (U.obj ∘ fun (a : α) ↦ (s.proj a).f i) a)
have w : Hom.f.{w, v, u}
    ({ f := fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i, φ := φ : Hom.{w, v, u} s.pt (Cone.pt (U.powerFan α)) } ≫
      Fan.proj (U.powerFan α) a) =
  (s.proj a).f
Tactic: obtain ⟨_, hm⟩ := hm
Cleared hypotheses: hm