awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [∀ (i : ι), HasColimit (F i)],
    ∃ (c : (i : ι) → Cocone (F i)) (x : (i : ι) → IsColimit (c i)),
      Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
c' : (i : ι) → Cocone (F i)
hc' : (i : ι) → IsColimit (c' i)
h_1 : Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c'))
e : Iso (C := Cocone (pointwiseProduct (I := J) F)) (coconePointwiseProduct (I := J) c)
  (coconePointwiseProduct (I := J) c') :=
  coconePointwiseProductIso (I := J) F fun (i : ι) ↦ (hc i).uniqueUpToIso (hc' i)
rwa rwa₁ rwa₂ rwa₃ : Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c'))
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
rwa [(IsColimit.equivIsoColimit e).nonempty_congr]

Premises used: CategoryTheory.Limits.IsColimit.equivIsoColimit, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ (J : ι → Type w) [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [inst_4 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct (I := J) F)),
      IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
        (colimitPointwiseProductToProductColimit (I := J) F)
⊢ IsIPCOfShape.{w, u_2, v_1, u_1} ι C

Tactic:
.of_forall_exists fun J _ _ F _ ↦ ?_

Premises used: CategoryTheory.Limits.IsIPCOfShape.of_forall_exists
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ (J : ι → Type w) [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [inst_4 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct (I := J) F)),
      IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
        (colimitPointwiseProductToProductColimit (I := J) F)
refine :
  ∀ (J : ι → Type w) (x : (i : ι) → SmallCategory (J i)),
    (∀ (i : ι), IsFiltered.{w, w} (J i)) →
      ∀ (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C),
        (∀ (i : ι), HasColimit (F i)) →
          ∃ (c : (i : ι) → Cocone (F i)) (x_3 : (i : ι) → IsColimit (c i)),
            Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
⊢ IsIPCOfShape.{w, u_2, v_1, u_1} ι C

Tactic:
refine .of_forall_exists fun J _ _ F _ ↦ ?_
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ (J : ι → Type w) [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [inst_4 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct (I := J) F)),
      IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
        (colimitPointwiseProductToProductColimit (I := J) F)
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
h_1 : ∀ (i : ι), HasColimit (F i)
⊢ ∃ (c : (i : ι) → Cocone (F i)) (x_1 : (i : ι) → IsColimit (c i)),
    Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
⟨fun i ↦ colimit.cocone _, fun i ↦ colimit.isColimit _, ?_⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, Exists.intro, CategoryTheory.Limits.colimit.cocone
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ (J : ι → Type w) [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [inst_4 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct (I := J) F)),
      IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
        (colimitPointwiseProductToProductColimit (I := J) F)
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
h_1 : ∀ (i : ι), HasColimit (F i)
refine :
  Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))
⊢ ∃ (c : (i : ι) → Cocone (F i)) (x_1 : (i : ι) → IsColimit (c i)),
    Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
refine ⟨fun i ↦ colimit.cocone _, fun i ↦ colimit.isColimit _, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ (J : ι → Type w) [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [inst_4 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct (I := J) F)),
      IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
        (colimitPointwiseProductToProductColimit (I := J) F)
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
h_1 : ∀ (i : ι), HasColimit (F i)
⊢ HasColimit (pointwiseProduct (I := J) F)

Tactic:
obtain ⟨_, h⟩ := H J F
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ (J : ι → Type w) [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [inst_4 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct (I := J) F)),
      IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
        (colimitPointwiseProductToProductColimit (I := J) F)
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
h_1 : ∀ (i : ι), HasColimit (F i)
w : HasColimit (pointwiseProduct (I := J) F)
⊢ IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
    (colimitPointwiseProductToProductColimit (I := J) F)

Tactic:
obtain ⟨_, h⟩ := H J F
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ (J : ι → Type w) [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [inst_4 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct (I := J) F)),
      IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
        (colimitPointwiseProductToProductColimit (I := J) F)
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h_1 : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
h_2 : ∀ (i : ι), HasColimit (F i)
w : HasColimit (pointwiseProduct (I := J) F)
h :
  IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
    (colimitPointwiseProductToProductColimit (I := J) F)
rwa rwa₁ rwa₂ rwa₃ :
  IsIso (X := (colimit.cocone (pointwiseProduct (I := J) F)).pt) (Y :=
    Cocone.pt (J := (i : ι) → J i) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))
    (IsColimit.desc (colimit.isColimit (pointwiseProduct (I := J) F))
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))
⊢ Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))

Tactic:
rwa [IsColimit.nonempty_isColimit_iff_isIso_desc (colimit.isColimit _)]

Premises used: CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc, CategoryTheory.Limits.colimit.isColimit
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
ι' : Type u_3
inst_2 : HasProductsOfShape.{u_3, u_1, v_1} ι' C
inst_3 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x : (i : ι') → SmallCategory (J i)
h : ∀ (i : ι'), IsFiltered.{w, w} (J i)
F : (i : ι') → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
obtain :
  ∀
    (h :
      IsColimit (J := (i : ι) → J ((e : (a : ι) → ι') i)) (C := C) (F :=
        pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i))
        (coconePointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ c ((e : (a : ι) → ι') i))),
    Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
obtain ⟨h⟩ := nonempty_isColimit fun i : ι ↦ hc (e i)

Premises used: CategoryTheory.Limits.IsIPCOfShape.nonempty_isColimit, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
ι' : Type u_3
inst_2 : HasProductsOfShape.{u_3, u_1, v_1} ι' C
inst_3 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x : (i : ι') → SmallCategory (J i)
h_1 : ∀ (i : ι'), IsFiltered.{w, w} (J i)
F : (i : ι') → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h :
  IsColimit (J := (i : ι) → J ((e : (a : ι) → ι') i)) (C := C) (F :=
    pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i))
    (coconePointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ c ((e : (a : ι) → ι') i))
val : IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c)
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
ι' : Type u_3
inst_2 : HasProductsOfShape.{u_3, u_1, v_1} ι' C
inst_3 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x : (i : ι') → SmallCategory (J i)
h_1 : ∀ (i : ι'), IsFiltered.{w, w} (J i)
F : (i : ι') → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h :
  IsColimit (J := (i : ι) → J ((e : (a : ι) → ι') i)) (C := C) (F :=
    pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i))
    (coconePointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ c ((e : (a : ι) → ι') i))
apply :
  (Equivalence.functor (Equivalence.symm (Pi.equivalenceOfEquiv J e)) ⋙
      pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i)) ≅
    pointwiseProduct (I := J) F
apply₁ :
  Iso (C := Cocone (pointwiseProduct (I := J) F))
    (Functor.obj (C :=
      Cocone (C := C)
        (Equivalence.functor (Equivalence.symm (Pi.equivalenceOfEquiv J e)) ⋙
          pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i)))
      (Cocone.precompose (Iso.inv (Pi.equivalenceOfEquivCompPointwiseProduct (I := J) F e)))
      (Cocone.whisker (Equivalence.functor (Equivalence.symm (Pi.equivalenceOfEquiv J e)))
        (coconePointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ c ((e : (a : ι) → ι') i))))
    (coconePointwiseProduct (I := J) c)
⊢ IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c)

Tactic:
apply IsColimit.equivOfNatIsoOfIso _ _ _ _ <|
        h.whiskerEquivalence (Pi.equivalenceOfEquiv J e).symm

Premises used: CategoryTheory.Pi.equivalenceOfEquiv, CategoryTheory.Limits.IsColimit.whiskerEquivalence, CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
ι' : Type u_3
inst_2 : HasProductsOfShape.{u_3, u_1, v_1} ι' C
inst_3 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x : (i : ι') → SmallCategory (J i)
h_1 : ∀ (i : ι'), IsFiltered.{w, w} (J i)
F : (i : ι') → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h :
  IsColimit (J := (i : ι) → J ((e : (a : ι) → ι') i)) (C := C) (F :=
    pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i))
    (coconePointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ c ((e : (a : ι) → ι') i))
⊢ (Equivalence.functor (Equivalence.symm (Pi.equivalenceOfEquiv J e)) ⋙
      pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i)) ≅
    pointwiseProduct (I := J) F

Tactic:
exact (Pi.equivalenceOfEquivCompPointwiseProduct F e)

Premises used: CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
ι' : Type u_3
inst_2 : HasProductsOfShape.{u_3, u_1, v_1} ι' C
inst_3 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x : (i : ι') → SmallCategory (J i)
h_1 : ∀ (i : ι'), IsFiltered.{w, w} (J i)
F : (i : ι') → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h :
  IsColimit (J := (i : ι) → J ((e : (a : ι) → ι') i)) (C := C) (F :=
    pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i))
    (coconePointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ c ((e : (a : ι) → ι') i))
⊢ Iso (C := Cocone (pointwiseProduct (I := J) F))
    (Functor.obj (C :=
      Cocone (C := C)
        (Equivalence.functor (Equivalence.symm (Pi.equivalenceOfEquiv J e)) ⋙
          pointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ F ((e : (a : ι) → ι') i)))
      (Cocone.precompose (Iso.inv (Pi.equivalenceOfEquivCompPointwiseProduct (I := J) F e)))
      (Cocone.whisker (Equivalence.functor (Equivalence.symm (Pi.equivalenceOfEquiv J e)))
        (coconePointwiseProduct (I := fun (i : ι) ↦ J ((e : (a : ι) → ι') i)) fun (i : ι) ↦ c ((e : (a : ι) → ι') i))))
    (coconePointwiseProduct (I := J) c)

Tactic:
exact (Cocone.ext (Pi.whiskerEquiv e fun _ ↦ Iso.refl _).symm).symm

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι_1 : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι_1 C
inst_2 : HasProducts.{w, v_1, u_1} C
inst_3 : HasFilteredColimitsOfSize.{w, w, v_1, u_1} C
inst_4 : IsIPC.{w, v_1, u_1, w} C
ι : Type u_3
inst_5 : Small.{w, u_3} ι
inst_6 : HasProductsOfShape.{u_3, u_1, v_1} ι C
suffices : IsIPCOfShape.{w, w, v_1, u_1} (Shrink.{w, u_3} ι) C
⊢ IsIPCOfShape.{w, u_3, v_1, u_1} ι C

Tactic:
suffices IsIPCOfShape (Shrink.{w} ι) C from .of_equiv (equivShrink ι).symm
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι_1 : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι_1 C
inst_2 : HasProducts.{w, v_1, u_1} C
inst_3 : HasFilteredColimitsOfSize.{w, w, v_1, u_1} C
inst_4 : IsIPC.{w, v_1, u_1, w} C
ι : Type u_3
inst_5 : Small.{w, u_3} ι
inst_6 : HasProductsOfShape.{u_3, u_1, v_1} ι C
⊢ IsIPCOfShape.{w, w, v_1, u_1} (Shrink.{w, u_3} ι) C

Tactic:
apply IsIPC.isIPCOfShape

Premises used: CategoryTheory.Limits.IsIPC.isIPCOfShape
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
⊢ IsIso (X := colimit (pointwiseProduct (I := I) F)) (Y := ∏ᶜ fun (s : α) ↦ colimit (F s))
    (colimitPointwiseProductToProductColimit (I := I) F)

Tactic:
(isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩

Premises used: Iff.mpr, CategoryTheory.isIso_iff_bijective, And.intro
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
refine_1 :
  ∀ (y y' : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))
    (hy :
      Eq (α := (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
              (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
            y :
          (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
              (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
            y' :
          (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))),
    y = y'
refine_2 :
  ∀ (x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))),
    ∃ (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))),
      (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
            (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
              (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
          a =
        x
⊢ IsIso (X := colimit (pointwiseProduct (I := I) F)) (Y := ∏ᶜ fun (s : α) ↦ colimit (F s))
    (colimitPointwiseProductToProductColimit (I := I) F)

Tactic:
refine (isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩

Premises used: Iff.mpr, CategoryTheory.isIso_iff_bijective, And.intro
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))
hy :
  Eq (α := (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y' :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
refine_1 :
  ∀ (ky : (i : α) → I i) (yk₀ : (pointwiseProduct (I := I) F).obj ky)
    (hyk₀ :
      (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky) :
            (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky)) →
              (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
          yk₀ =
        y),
    y = y'
⊢ y = y'

Tactic:
obtain ⟨ky, yk₀, hyk₀⟩ := Types.jointly_surjective' y

Premises used: CategoryTheory.Limits.Types.jointly_surjective'
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))
hy :
  Eq (α := (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
            (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
        y' :
      (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
ky : (i : α) → I i
yk₀ : (pointwiseProduct (I := I) F).obj ky
hyk₀ :
  (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky) :
        (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky)) →
          (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
      yk₀ =
    y
refine_1 :
  ∀ (ky' : (i : α) → I i) (yk₀' : (pointwiseProduct (I := I) F).obj ky')
    (hyk₀' :
      (hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky') :
            (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky')) →
              (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
          yk₀' =
        y'),
    y = y'
⊢ y = y'

Tactic:
obtain ⟨ky', yk₀', hyk₀'⟩ := Types.jointly_surjective' y'

Premises used: CategoryTheory.Limits.Types.jointly_surjective'