awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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 ⋯) =
      (x.proj x_1).φ i
⊢ 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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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 : α
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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 : α
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 ⋯) =
    (x.proj x_1).φ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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
⊢ 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

Tactic:
obtain ⟨f, φ⟩ := m
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
h : ∀ (i : s.pt.I), f i = fun (a : α) ↦ (s.proj a).f i
⊢ f = fun (i : s.pt.I) (a : α) ↦ (s.proj a).f i

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
h : ∀ (a : α), f i a = (s.proj a).f i
⊢ f i = fun (a : α) ↦ (s.proj a).f i

Tactic:
ext a
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
a : α
⊢ f i a = (s.proj a).f i

Tactic:
congr_fun (congr_arg FormalCoproduct.Hom.f (hm a)) i

Premises used: CategoryTheory.Limits.FormalCoproduct.Hom.f, congr_arg, congr_fun
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
a : α
⊢ f i a = (s.proj a).f i

Tactic:
exact congr_fun (congr_arg FormalCoproduct.Hom.f (hm a)) i

Premises used: CategoryTheory.Limits.FormalCoproduct.Hom.f, congr_arg, congr_fun
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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
⊢ { 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 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

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.FormalCoproduct.Hom.f, rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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 ⋯)
      (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)
⊢ { 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:
ext i
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
⊢ { 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:
rfl
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
h₂ : φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i)) = Pi.lift fun (a : α) ↦ (s.proj a).φ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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)
⊢ φ i ≫ 𝟙 (piObj.{0, v, u} (β := α) (U.obj ∘ fun (a : α) ↦ (s.proj a).f i)) = Pi.lift fun (a : α) ↦ (s.proj a).φ i

Tactic:
ext a
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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 : α
⊢ { 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
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
⊢ ∃ (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

Tactic:
rw [hom_ext_iff] at hm

Premises used: CategoryTheory.Limits.FormalCoproduct.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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
⊢ ∀ (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

Tactic:
obtain ⟨_, hm⟩ := hm
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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 : α
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
hm :
  ∀ (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)

Tactic:
simpa using hm i
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
Goal:
C : Type u
inst : Category.{v, u} C
U V W : FormalCoproduct.{w, u} C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
h₁ : ∀ (x : (power.{w, t, v, u} U α).I), Hom.f (powerMap (f ≫ g) α) x = Hom.f (powerMap f α ≫ powerMap g α) x
h₂ :
  ∀ (i : (power.{w, t, v, u} U α).I),
    Eq (α := (power.{w, t, v, u} U α).obj i ⟶ (power.{w, t, v, u} W α).obj (Hom.f (powerMap f α ≫ powerMap g α) i))
      (CategoryStruct.comp (Y := (power.{w, t, v, u} W α).obj (Hom.f (powerMap (f ≫ g) α) i))
        (Hom.φ (powerMap (f ≫ g) α) i) (eqToHom ⋯))
      (Hom.φ (powerMap f α ≫ powerMap g α) i)
⊢ Eq (α := power.{w, t, v, u} U α ⟶ power.{w, t, v, u} W α) (powerMap (f ≫ g) α) (powerMap f α ≫ powerMap g α)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
Goal:
C : Type u
inst : Category.{v, u} C
U V W : FormalCoproduct.{w, u} C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
x : (power.{w, t, v, u} U α).I
h₁ h₂ h₃ h₄ : Hom.f (powerMap (f ≫ g) α) x = Hom.f (powerMap f α ≫ powerMap g α) x
⊢ Hom.f (powerMap (f ≫ g) α) x = Hom.f (powerMap f α ≫ powerMap g α) x

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
Goal:
C : Type u
inst : Category.{v, u} C
U V W : FormalCoproduct.{w, u} C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
i : (power.{w, t, v, u} U α).I
h₂ :
  Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ piObj.{t, v, u} (W.obj ∘ g.f ∘ f.f ∘ i))
    ((Pi.map fun (a : α) ↦ f.φ (i a) ≫ g.φ (f.f (i a))) ≫ 𝟙 (piObj.{t, v, u} (W.obj ∘ (f ≫ g).f ∘ i)))
    (CategoryStruct.comp (Y := piObj.{t, v, u} (V.obj ∘ f.f ∘ i)) (Pi.map fun (a : α) ↦ f.φ (i a))
      (Pi.map fun (a : α) ↦ g.φ (f.f (i a))))
⊢ Eq (α := (power.{w, t, v, u} U α).obj i ⟶ (power.{w, t, v, u} W α).obj (Hom.f (powerMap f α ≫ powerMap g α) i))
    (CategoryStruct.comp (Y := (power.{w, t, v, u} W α).obj (Hom.f (powerMap (f ≫ g) α) i))
      (Hom.φ (powerMap (f ≫ g) α) i) (eqToHom ⋯))
    (Hom.φ (powerMap f α ≫ powerMap g α) i)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
Goal:
C : Type u
inst : Category.{v, u} C
U V W : FormalCoproduct.{w, u} C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
i : (power.{w, t, v, u} U α).I
h₂ :
  ∀ (b : α),
    Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ (W.obj ∘ g.f ∘ f.f ∘ i) b)
      (((Pi.map fun (a : α) ↦ f.φ (i a) ≫ g.φ (f.f (i a))) ≫ 𝟙 (piObj.{t, v, u} (W.obj ∘ (f ≫ g).f ∘ i))) ≫
        Pi.π (W.obj ∘ g.f ∘ f.f ∘ i) b)
      (CategoryStruct.comp (Y := piObj.{t, v, u} (W.obj ∘ g.f ∘ f.f ∘ i))
        (CategoryStruct.comp (Y := piObj.{t, v, u} (V.obj ∘ f.f ∘ i)) (Pi.map fun (a : α) ↦ f.φ (i a))
          (Pi.map fun (a : α) ↦ g.φ (f.f (i a))))
        (Pi.π (W.obj ∘ g.f ∘ f.f ∘ i) b))
⊢ Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ piObj.{t, v, u} (W.obj ∘ g.f ∘ f.f ∘ i))
    ((Pi.map fun (a : α) ↦ f.φ (i a) ≫ g.φ (f.f (i a))) ≫ 𝟙 (piObj.{t, v, u} (W.obj ∘ (f ≫ g).f ∘ i)))
    (CategoryStruct.comp (Y := piObj.{t, v, u} (V.obj ∘ f.f ∘ i)) (Pi.map fun (a : α) ↦ f.φ (i a))
      (Pi.map fun (a : α) ↦ g.φ (f.f (i a))))

Tactic:
ext