awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J_1 : Type u₁
K : Type u₂
inst : SmallCategory J_1
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J_1
F_1 : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
c : Cone F
hc : IsLimit c
trans : Iso (C := Cone (F ⋙ colim)) (mapCone colim c) (mapCone colim (limit.cone F))
⊢ mapCone colim c ≅ limit.cone (F ⋙ colim)
have trans₁ : mapCone colim (limit.cone F) ≅ limit.cone (F ⋙ colim)
Tactic: trans colim.mapCone (limit.cone F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
C : Type u
inst_5 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_6 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory C FC (CC := CC)
inst_8 : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
inst_9 : PreservesColimitsOfShape.{v₂, u₂, v, v, u, v + 1} K (forget C (FC := FC) (CC := CC))
inst_10 : HasFiniteLimits.{v, u} C
inst_11 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_12 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
⊢ PreservesFiniteLimits (C := Functor.{v₂, v, u₂, u} K C) colim
have h : ∀ (J : Type v) {𝒥 : SmallCategory J} (x : FinCategory J),
  PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v}
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst_1 : (i : α) → Category.{v_1, u_2} (I i)
inst_2 : HasProductsOfShape.{u_1, u, v} α C
F : (i : α) → Functor.{v_1, v, u_2, u} (I i) C
c c' : (i : α) → Cocone (F i)
e : (i : α) → c i ≅ c' i
i : (i : α) → I i
⊢ Eq (α :=
    (pointwiseProduct (I := I) F).obj i ⟶
      Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c'))
    (CategoryStruct.comp (Y := Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c))
        (NatTrans.app (Cocone.ι (coconePointwiseProduct (I := I) c)) i :
          (pointwiseProduct (I := I) F).obj i ⟶
            Functor.obj
              (Functor.obj (Functor.const ((i : α) → I i))
                (Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c)))
              i)
        (Iso.hom (Pi.mapIso fun (i : α) ↦ (Cocone.forget (F i)).mapIso (e i))) :
      (pointwiseProduct (I := I) F).obj i ⟶
        Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c'))
    (NatTrans.app (Cocone.ι (coconePointwiseProduct (I := I) c')) i :
      (pointwiseProduct (I := I) F).obj i ⟶
        Functor.obj
          (Functor.obj (Functor.const ((i : α) → I i))
            (Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c')))
          i)
have dsimp : Eq.{v + 1} (α :=
  piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶ piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
  (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
      (CategoryStruct.comp (Y :=
          piObj.{u_1, v, u}
            (Functor.obj
              (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c i).pt) i))
          (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c i).ι) i))
          (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)) :
        piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
          piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
      (Iso.hom (Pi.mapIso fun (i : α) ↦ (Cocone.forget (F i)).mapIso (e i)) :
        Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
          (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
    piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
      piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
  (CategoryStruct.comp (Y :=
      piObj.{u_1, v, u}
        (Functor.obj
          (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c' i).pt) i))
      (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c' i).ι) i))
      (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
    piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
      piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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
inst_2 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst_3 : (i : ι) → SmallCategory (J i)
inst_4 : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
inst_5 : ∀ (i : ι), HasColimit (F i)
inst_6 : 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))
    (IsColimit.desc (colimit.isColimit (pointwiseProduct (I := J) F))
        (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)) :
      (colimit.cocone (pointwiseProduct (I := J) F)).pt ⟶
        Cocone.pt (J := (i : ι) → J i) (F := pointwiseProduct (I := J) F)
          (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)))
have refine : Nonempty
  (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
    (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)))
Tactic: refine ((colimit.isColimit (pointwiseProduct F)).nonempty_isColimit_iff_isIso_desc).mp ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (hypothesis)
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)
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
have this : ∀ (i : ι), HasColimit (F i)
Tactic: have (i : ι) : HasColimit (F i) := ⟨_, hc i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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)
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
have obtain : ∀ (c' : (i : ι) → Cocone (F i)) (hc' : (i : ι) → IsColimit (c' 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 ⟨c', hc', _⟩ := H F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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
have 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))
Tactic: refine .of_forall_exists fun J _ _ F _ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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))
have refine : Nonempty
  (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
    (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))
Tactic: refine ⟨fun i ↦ colimit.cocone _, fun i ↦ colimit.isColimit _, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (hypothesis)
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)
⊢ Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))
have w : HasColimit (pointwiseProduct (I := J) F)
Tactic: obtain ⟨_, h⟩ := H J F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (hypothesis)
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)
⊢ Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))
have 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)
Tactic: obtain ⟨_, h⟩ := H J F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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)
⊢ Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (i : ι) ↦ colimit.cocone (F i)))
have 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)))
Tactic: rwa [IsColimit.nonempty_isColimit_iff_isIso_desc (colimit.isColimit _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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)
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
have 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))
Tactic: obtain ⟨h⟩ := nonempty_isColimit fun i : ι ↦ hc (e i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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))
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
have val : IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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))
⊢ IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c)
have 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
Tactic: apply IsColimit.equivOfNatIsoOfIso _ _ _ _ <|
        h.whiskerEquivalence (Pi.equivalenceOfEquiv J e).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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
⊢ IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c)
have 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)
Tactic: apply IsColimit.equivOfNatIsoOfIso _ _ _ _ <|
        h.whiskerEquivalence (Pi.equivalenceOfEquiv J e).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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, u_3, v_1, u_1} ι C
have suffices : IsIPCOfShape.{w, w, v_1, u_1} (Shrink.{w, u_3} ι) C
Tactic: suffices IsIPCOfShape (Shrink.{w} ι) C from .of_equiv (equivShrink ι).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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)
have 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'
Tactic: refine (isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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'
⊢ IsIso (X := colimit (pointwiseProduct (I := I) F)) (Y := ∏ᶜ fun (s : α) ↦ colimit (F s))
    (colimitPointwiseProductToProductColimit (I := I) F)
have 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
Tactic: refine (isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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)))
⊢ y = y'
have 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'
Tactic: obtain ⟨ky, yk₀, hyk₀⟩ := Types.jointly_surjective' y