awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
b : α
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)))
⊢ 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:
simp only [Category.comp_id, Category.assoc, Pi.map_π, Function.comp_apply,
      Pi.map_π_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Pi.map_π_assoc, Function.comp_apply, CategoryTheory.Limits.Pi.map_π
-- 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
b : α
⊢ 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:
apply Pi.map_π

Premises used: CategoryTheory.Limits.Pi.map_π
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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)
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 ⋯))
      (Hom.φ (CategoryStruct.comp (Y := power.{w, t, v, u} U β) (U.mapPower g) (U.mapPower f)) i)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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 : β → γ
x : (power.{w, t, v, u} U γ).I
h₁ h₂ h₃ h₄ :
  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 α).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:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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)))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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))
⊢ 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:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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)
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 ⋯))
      (Hom.φ (powerMap f β ≫ V.mapPower g) i)
⊢ Eq (α := power.{w, t, v, u} U β ⟶ power.{w, t, v, u} V α) (U.mapPower g ≫ powerMap f α) (powerMap f β ≫ V.mapPower g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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 : α → β
x : (power.{w, t, v, u} U β).I
h₁ h₂ h₃ h₄ :
  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} V α).I) (Hom.f (U.mapPower g ≫ powerMap f α) x) (Hom.f (powerMap f β ≫ V.mapPower g) x)

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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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))
⊢ 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:
ext
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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:
simp [Function.comp_def]

Premises used: Function.comp_def
-- 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
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
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 ⋯))
      (Hom.φ (U.powerπ (f a)) i)
⊢ 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))

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
inst_2 : HasProductsOfShape.{0, u, v} β C
f : α → β
a : α
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:
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
inst_2 : HasProductsOfShape.{0, u, v} β C
f : α → β
a : α
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 ⋯))
    (Hom.φ (U.powerπ (f a)) i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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 := ⋯ }
        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 := ⋯ }
          {
            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 := ⋯ })
        x_2)
⊢ 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 := ⋯ })

Tactic:
ext : 2
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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 := ⋯ }
      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 := ⋯ }
        {
          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 := ⋯ })
      x_2)

Tactic:
simp [types_comp]

Premises used: CategoryTheory.types_comp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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 := ⋯ }
        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 := ⋯ }
          {
            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 := ⋯ })
        n)
⊢ 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 := ⋯ })

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
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
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 := ⋯ }
      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 := ⋯ }
        {
          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 := ⋯ })
      n)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
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 : ℕ
dsimp :
  HasWidePullback (Functor.obj (incl C) T) (fun (x : Fin (n + 1)) ↦ U) fun (x : Fin (n + 1)) ↦
    (isTerminalIncl T hT).from U
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
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 : ℕ
⊢ 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))⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
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 : ℕ
this : HasProduct (C := FormalCoproduct.{w, u} C) fun (x : Fin (n + 1)) ↦ U
⊢ HasWidePullback (Functor.obj (incl C) T) (fun (x : Fin (n + 1)) ↦ U) fun (x : Fin (n + 1)) ↦
    (isTerminalIncl T hT).from U

Tactic:
hasWidePullback_of_isTerminal _ (isTerminalIncl _ hT)

Premises used: CategoryTheory.Limits.FormalCoproduct.isTerminalIncl, CategoryTheory.Limits.hasWidePullback_of_isTerminal
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
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 : ℕ
this : HasProduct (C := FormalCoproduct.{w, u} C) fun (x : Fin (n + 1)) ↦ U
⊢ HasWidePullback (Functor.obj (incl C) T) (fun (x : Fin (n + 1)) ↦ U) fun (x : Fin (n + 1)) ↦
    (isTerminalIncl T hT).from U

Tactic:
exact hasWidePullback_of_isTerminal _ (isTerminalIncl _ hT)

Premises used: CategoryTheory.Limits.FormalCoproduct.isTerminalIncl, CategoryTheory.Limits.hasWidePullback_of_isTerminal