awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 ≫ 𝟙 (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₁ : ∀ (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: obtain ⟨_, hm⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
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
⊢ Eq (α := power.{w, t, v, u} U α ⟶ power.{w, t, v, u} W α) (powerMap (f ≫ g) α) (powerMap f α ≫ powerMap g α)
have h₁ : ∀ (x : (power.{w, t, v, u} U α).I), Hom.f (powerMap (f ≫ g) α) x = Hom.f (powerMap f α ≫ powerMap g α) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
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
⊢ Eq (α := power.{w, t, v, u} U α ⟶ power.{w, t, v, u} W α) (powerMap (f ≫ g) α) (powerMap f α ≫ powerMap g α)
have 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 sorry))
    (Hom.φ (powerMap f α ≫ powerMap g α) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
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
⊢ 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)
have 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))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
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
⊢ 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))))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
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
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))
have h₂ : Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ W.obj (g.f (f.f (i b))))
  (CategoryStruct.comp (Y := piObj.{t, v, u} (W.obj ∘ g.f ∘ f.f ∘ i)) (Pi.map fun (a : α) ↦ f.φ (i a) ≫ g.φ (f.f (i a)))
    (Pi.π (W.obj ∘ g.f ∘ f.f ∘ i) b))
  (Pi.π (U.obj ∘ i) b ≫ f.φ (i b) ≫ g.φ (f.f (i b)))
Tactic: simp only [Category.comp_id, Category.assoc, Pi.map_π, Function.comp_apply,
      Pi.map_π_assoc]
-- 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 t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
inst_3 : HasProductsOfShape.{t, u, v} γ C
f : α → β
g : β → γ
⊢ Eq (α := power.{w, t, v, u} U γ ⟶ power.{w, t, v, u} U α) (U.mapPower (g ∘ f))
    (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f))
have h₁ : ∀ (x : (power.{w, t, v, u} U γ).I),
  Eq (α := (power.{w, t, v, u} U α).I) (Hom.f (U.mapPower (g ∘ f)) x)
    (Hom.f (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f)) x)
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 t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
inst_3 : HasProductsOfShape.{t, u, v} γ C
f : α → β
g : β → γ
h₁ :
  ∀ (x : (power.{w, t, v, u} U γ).I),
    Eq (α := (power.{w, t, v, u} U α).I) (Hom.f (U.mapPower (g ∘ f)) x)
      (Hom.f (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f)) x)
⊢ Eq (α := power.{w, t, v, u} U γ ⟶ power.{w, t, v, u} U α) (U.mapPower (g ∘ f))
    (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f))
have h₂ : ∀ (i : (power.{w, t, v, u} U γ).I),
  Eq (α :=
    (power.{w, t, v, u} U γ).obj i ⟶
      (power.{w, t, v, u} U α).obj
        (Hom.f (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f)) i))
    (CategoryStruct.comp (Y := (power.{w, t, v, u} U α).obj (Hom.f (U.mapPower (g ∘ f)) i))
      (Hom.φ (U.mapPower (g ∘ f)) i) (eqToHom sorry))
    (Hom.φ (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f)) 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 t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
inst_3 : HasProductsOfShape.{t, u, v} γ C
f : α → β
g : β → γ
i : (power.{w, t, v, u} U γ).I
⊢ Eq (α :=
    (power.{w, t, v, u} U γ).obj i ⟶
      (power.{w, t, v, u} U α).obj
        (Hom.f (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f)) i))
    (CategoryStruct.comp (Y := (power.{w, t, v, u} U α).obj (Hom.f (U.mapPower (g ∘ f)) i))
      (Hom.φ (U.mapPower (g ∘ f)) i) (eqToHom ⋯))
    (Hom.φ (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f)) i)
have h₂ : Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ piObj.{t, v, u} (U.obj ∘ (i ∘ g) ∘ f))
  ((Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i) (g (f x))) ≫ 𝟙 (piObj.{t, v, u} (U.obj ∘ i ∘ g ∘ f)))
  (CategoryStruct.comp (Y := piObj.{t, v, u} (U.obj ∘ i ∘ g)) (Pi.lift fun (x : β) ↦ Pi.π (U.obj ∘ i) (g x))
    (Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i ∘ g) (f x)))
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 t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
inst_3 : HasProductsOfShape.{t, u, v} γ C
f : α → β
g : β → γ
i : (power.{w, t, v, u} U γ).I
⊢ Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ piObj.{t, v, u} (U.obj ∘ (i ∘ g) ∘ f))
    ((Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i) (g (f x))) ≫ 𝟙 (piObj.{t, v, u} (U.obj ∘ i ∘ g ∘ f)))
    (CategoryStruct.comp (Y := piObj.{t, v, u} (U.obj ∘ i ∘ g)) (Pi.lift fun (x : β) ↦ Pi.π (U.obj ∘ i) (g x))
      (Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i ∘ g) (f x)))
have h₂ : ∀ (b : α),
  Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ (U.obj ∘ (i ∘ g) ∘ f) b)
    (((Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i) (g (f x))) ≫ 𝟙 (piObj.{t, v, u} (U.obj ∘ i ∘ g ∘ f))) ≫
      Pi.π (U.obj ∘ (i ∘ g) ∘ f) b)
    (CategoryStruct.comp (Y := piObj.{t, v, u} (U.obj ∘ (i ∘ g) ∘ f))
      (CategoryStruct.comp (Y := piObj.{t, v, u} (U.obj ∘ i ∘ g)) (Pi.lift fun (x : β) ↦ Pi.π (U.obj ∘ i) (g x))
        (Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i ∘ g) (f x)))
      (Pi.π (U.obj ∘ (i ∘ g) ∘ f) b))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U V : FormalCoproduct.{w, u} C
f : U ⟶ V
α β : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
g : α → β
⊢ Eq (α := power.{w, t, v, u} U β ⟶ power.{w, t, v, u} V α) (U.mapPower g ≫ powerMap f α) (powerMap f β ≫ V.mapPower g)
have h₁ : ∀ (x : (power.{w, t, v, u} U β).I),
  Eq (α := (power.{w, t, v, u} V α).I) (Hom.f (U.mapPower g ≫ powerMap f α) x) (Hom.f (powerMap f β ≫ V.mapPower g) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U V : FormalCoproduct.{w, u} C
f : U ⟶ V
α β : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
g : α → β
h₁ :
  ∀ (x : (power.{w, t, v, u} U β).I),
    Eq (α := (power.{w, t, v, u} V α).I) (Hom.f (U.mapPower g ≫ powerMap f α) x) (Hom.f (powerMap f β ≫ V.mapPower g) x)
⊢ Eq (α := power.{w, t, v, u} U β ⟶ power.{w, t, v, u} V α) (U.mapPower g ≫ powerMap f α) (powerMap f β ≫ V.mapPower g)
have h₂ : ∀ (i : (power.{w, t, v, u} U β).I),
  Eq (α := (power.{w, t, v, u} U β).obj i ⟶ (power.{w, t, v, u} V α).obj (Hom.f (powerMap f β ≫ V.mapPower g) i))
    (CategoryStruct.comp (Y := (power.{w, t, v, u} V α).obj (Hom.f (U.mapPower g ≫ powerMap f α) i))
      (Hom.φ (U.mapPower g ≫ powerMap f α) i) (eqToHom sorry))
    (Hom.φ (powerMap f β ≫ V.mapPower g) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U V : FormalCoproduct.{w, u} C
f : U ⟶ V
α β : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
g : α → β
i : (power.{w, t, v, u} U β).I
⊢ Eq (α := (power.{w, t, v, u} U β).obj i ⟶ (power.{w, t, v, u} V α).obj (Hom.f (powerMap f β ≫ V.mapPower g) i))
    (CategoryStruct.comp (Y := (power.{w, t, v, u} V α).obj (Hom.f (U.mapPower g ≫ powerMap f α) i))
      (Hom.φ (U.mapPower g ≫ powerMap f α) i) (eqToHom ⋯))
    (Hom.φ (powerMap f β ≫ V.mapPower g) i)
have h₂ : Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ piObj.{t, v, u} (V.obj ∘ (f.f ∘ i) ∘ g))
  (CategoryStruct.comp (Y := piObj.{t, v, u} (U.obj ∘ i ∘ g)) (Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i) (g x))
      (Pi.map fun (a : α) ↦ f.φ (i (g a))) ≫
    𝟙 (piObj.{t, v, u} (V.obj ∘ f.f ∘ i ∘ g)))
  (CategoryStruct.comp (Y := piObj.{t, v, u} (V.obj ∘ f.f ∘ i)) (Pi.map fun (a : β) ↦ f.φ (i a))
    (Pi.lift fun (x : α) ↦ Pi.π (V.obj ∘ f.f ∘ i) (g x)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
U V : FormalCoproduct.{w, u} C
f : U ⟶ V
α β : Type t
inst_1 : HasProductsOfShape.{t, u, v} α C
inst_2 : HasProductsOfShape.{t, u, v} β C
g : α → β
i : (power.{w, t, v, u} U β).I
⊢ Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ piObj.{t, v, u} (V.obj ∘ (f.f ∘ i) ∘ g))
    (CategoryStruct.comp (Y := piObj.{t, v, u} (U.obj ∘ i ∘ g)) (Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i) (g x))
        (Pi.map fun (a : α) ↦ f.φ (i (g a))) ≫
      𝟙 (piObj.{t, v, u} (V.obj ∘ f.f ∘ i ∘ g)))
    (CategoryStruct.comp (Y := piObj.{t, v, u} (V.obj ∘ f.f ∘ i)) (Pi.map fun (a : β) ↦ f.φ (i a))
      (Pi.lift fun (x : α) ↦ Pi.π (V.obj ∘ f.f ∘ i) (g x)))
have h₂ : ∀ (b : α),
  Eq (α := piObj.{t, v, u} (U.obj ∘ i) ⟶ (V.obj ∘ (f.f ∘ i) ∘ g) b)
    ((CategoryStruct.comp (Y := piObj.{t, v, u} (U.obj ∘ i ∘ g)) (Pi.lift fun (x : α) ↦ Pi.π (U.obj ∘ i) (g x))
          (Pi.map fun (a : α) ↦ f.φ (i (g a))) ≫
        𝟙 (piObj.{t, v, u} (V.obj ∘ f.f ∘ i ∘ g))) ≫
      Pi.π (V.obj ∘ (f.f ∘ i) ∘ g) b)
    (CategoryStruct.comp (Y := piObj.{t, v, u} (V.obj ∘ (f.f ∘ i) ∘ g))
      (CategoryStruct.comp (Y := piObj.{t, v, u} (V.obj ∘ f.f ∘ i)) (Pi.map fun (a : β) ↦ f.φ (i a))
        (Pi.lift fun (x : α) ↦ Pi.π (V.obj ∘ f.f ∘ i) (g x)))
      (Pi.π (V.obj ∘ (f.f ∘ i) ∘ g) b))
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
inst_2 : HasProductsOfShape.{0, u, v} β C
f : α → β
a : α
⊢ Eq (α := power.{w, 0, v, u} U β ⟶ U) (CategoryStruct.comp (Y := power.{w, 0, v, u} U α) (U.mapPower f) (U.powerπ a))
    (U.powerπ (f a))
have h₁ : ∀ (x : (power.{w, 0, v, u} U β).I),
  Hom.f (CategoryStruct.comp (Y := power.{w, 0, v, u} U α) (U.mapPower f) (U.powerπ a)) x = Hom.f (U.powerπ (f a)) x
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
inst_2 : HasProductsOfShape.{0, u, v} β C
f : α → β
a : α
h₁ :
  ∀ (x : (power.{w, 0, v, u} U β).I),
    Hom.f (CategoryStruct.comp (Y := power.{w, 0, v, u} U α) (U.mapPower f) (U.powerπ a)) x = Hom.f (U.powerπ (f a)) x
⊢ Eq (α := power.{w, 0, v, u} U β ⟶ U) (CategoryStruct.comp (Y := power.{w, 0, v, u} U α) (U.mapPower f) (U.powerπ a))
    (U.powerπ (f a))
have h₂ : ∀ (i : (power.{w, 0, v, u} U β).I),
  Eq (α := (power.{w, 0, v, u} U β).obj i ⟶ U.obj (Hom.f (U.powerπ (f a)) i))
    (CategoryStruct.comp (Y :=
      U.obj (Hom.f (CategoryStruct.comp (Y := power.{w, 0, v, u} U α) (U.mapPower f) (U.powerπ a)) i))
      (Hom.φ (CategoryStruct.comp (Y := power.{w, 0, v, u} U α) (U.mapPower f) (U.powerπ a)) i) (eqToHom sorry))
    (Hom.φ (U.powerπ (f a)) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{t, v, u} C
X Y Z : Type tᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := FormalCoproduct.{w, u} C ⥤ FormalCoproduct C) (powerFunctor.{w, t, v, u} (Opposite.unop X))
      (powerFunctor.{w, t, v, u} (Opposite.unop Z)))
    {
      app := fun (x_2 : FormalCoproduct.{w, u} C) ↦
        x_2.mapPower
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (x ≫ x_1).unop) :
            (a : (fun (X : Type t) ↦ X) (Opposite.unop Z)) → (fun (X : Type t) ↦ X) (Opposite.unop X)),
      naturality := ⋯ }
    (CategoryStruct.comp (Y := powerFunctor.{w, t, v, u} (Opposite.unop Y))
      {
        app := fun (x_2 : FormalCoproduct.{w, u} C) ↦
          x_2.mapPower
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x.unop) :
              (a : (fun (X : Type t) ↦ X) (Opposite.unop Y)) → (fun (X : Type t) ↦ X) (Opposite.unop X)),
        naturality := ⋯ }
      {
        app := fun (x : FormalCoproduct.{w, u} C) ↦
          x.mapPower
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x_1.unop) :
              (a : (fun (X : Type t) ↦ X) (Opposite.unop Z)) → (fun (X : Type t) ↦ X) (Opposite.unop Y)),
        naturality := ⋯ })
have w : ∀ (x_2 : FormalCoproduct.{w, u} C),
  Eq (α :=
    Functor.obj (powerFunctor.{w, t, v, u} (Opposite.unop X)) x_2 ⟶
      Functor.obj (powerFunctor.{w, t, v, u} (Opposite.unop Z)) x_2)
    (NatTrans.app
      {
        app := fun (x_3 : FormalCoproduct.{w, u} C) ↦
          x_3.mapPower
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (x ≫ x_1).unop) :
              (a : (fun (X : Type t) ↦ X) (Opposite.unop Z)) → (fun (X : Type t) ↦ X) (Opposite.unop X)),
        naturality := sorry }
      x_2)
    (NatTrans.app
      (CategoryStruct.comp (Y := powerFunctor.{w, t, v, u} (Opposite.unop Y))
        {
          app := fun (x_3 : FormalCoproduct.{w, u} C) ↦
            x_3.mapPower
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x.unop) :
                (a : (fun (X : Type t) ↦ X) (Opposite.unop Y)) → (fun (X : Type t) ↦ X) (Opposite.unop X)),
          naturality := sorry }
        {
          app := fun (x : FormalCoproduct.{w, u} C) ↦
            x.mapPower
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x_1.unop) :
                (a : (fun (X : Type t) ↦ X) (Opposite.unop Z)) → (fun (X : Type t) ↦ X) (Opposite.unop Y)),
          naturality := sorry })
      x_2)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
X Y Z : FormalCoproduct.{w, u} C
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := Quiver.Hom (V := SimplicialObject (FormalCoproduct.{w, u} C)) X.cech Z.cech)
    {
      app := fun (x_2 : SimplexCategoryᵒᵖ) ↦
        powerMap (x ≫ x_1)
          (ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop x_2)),
      naturality := ⋯ }
    (CategoryStruct.comp (Y := Y.cech)
      {
        app := fun (x_2 : SimplexCategoryᵒᵖ) ↦
          powerMap x
            (ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop x_2)),
        naturality := ⋯ }
      {
        app := fun (x : SimplexCategoryᵒᵖ) ↦
          powerMap x_1
            (ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop x)),
        naturality := ⋯ })
have h : ∀ (n : SimplexCategoryᵒᵖ),
  Eq (α := Functor.obj X.cech n ⟶ Functor.obj Z.cech n)
    (NatTrans.app
      {
        app := fun (x_2 : SimplexCategoryᵒᵖ) ↦
          powerMap (x ≫ x_1)
            (ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop x_2)),
        naturality := sorry }
      n)
    (NatTrans.app
      (CategoryStruct.comp (Y := Y.cech)
        {
          app := fun (x_2 : SimplexCategoryᵒᵖ) ↦
            powerMap x
              (ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop x_2)),
          naturality := sorry }
        {
          app := fun (x : SimplexCategoryᵒᵖ) ↦
            powerMap x_1
              (ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop x)),
          naturality := sorry })
      n)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
n : ℕ
⊢ HasWidePullback (Arrow.mk ((isTerminalIncl T hT).from U)).right
    (fun (x : Fin (n + 1)) ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).left) fun (x : Fin (n + 1)) ↦
    (Arrow.mk ((isTerminalIncl T hT).from U)).hom
have dsimp : HasWidePullback (Functor.obj (incl C) T) (fun (x : Fin (n + 1)) ↦ U) fun (x : Fin (n + 1)) ↦
  (isTerminalIncl T hT).from U
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
n : ℕ
⊢ HasWidePullback (Functor.obj (incl C) T) (fun (x : Fin (n + 1)) ↦ U) fun (x : Fin (n + 1)) ↦
    (isTerminalIncl T hT).from U
have this : HasProduct (C := FormalCoproduct.{w, u} C) fun (x : Fin (n + 1)) ↦ U
Tactic: have : HasProduct fun (x : Fin (n + 1)) ↦ U := ⟨⟨_, U.isLimitPowerFan (Fin (n + 1))⟩⟩