-- Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
theorem Types.isIso_colimitPointwiseProductToProductColimit (F : ∀ i, I i ⥤ Type u) :
    IsIso (colimitPointwiseProductToProductColimit F)

Proof state:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
yk' : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = colimit.ι (pointwiseProduct F) k yk
hyk₀' : colimit.ι (pointwiseProduct F) ky' yk₀' = colimit.ι (pointwiseProduct F) k yk'
hy :
  colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk) =
    colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk')
k' : (s : α) → I s
f : (s : α) → k s ⟶ k' s
hk' :
  ∀ (s : α),
    (F s).map (f s) (Pi.π (fun s => (F s).obj (k s)) s yk) = (F s).map (f s) (Pi.π (fun s => (F s).obj (k s)) s yk')
x✝ : Discrete α
s : α
⊢ limit.π (Discrete.functor fun s => (F s).obj (k' s)) { as := s } ((pointwiseProduct F).map f yk) =
    limit.π (Discrete.functor fun s => (F s).obj (k' s)) { as := s } ((pointwiseProduct F).map f yk')

Tactic:
simpa using hk' _

Result:
no goals

Proof state:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : ∏ᶜ fun s => colimit (F s)
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk : ∀ (s : α), colimit.ι (F s) (k s) (p s) = Pi.π (fun s => colimit (F s)) s x
x✝ : Discrete α
s : α
this :
  (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s => colimit (F s)) s)
      ((productIso fun s => (F s).obj (k s)).inv p) =
    (Pi.π (fun s => (F s).obj (k s)) s ≫ colimit.ι (F s) (k s)) ((productIso fun s => (F s).obj (k s)).inv p)
⊢ (Pi.π (fun s => (F s).obj (k s)) s ≫ colimit.ι (F s) (k s)) ((productIso fun s => (F s).obj (k s)).inv p) =
    limit.π (Discrete.functor fun s => colimit (F s)) { as := s } x

Tactic:
simpa using hk _

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
yk' : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = colimit.ι (pointwiseProduct F) k yk
hyk₀' : colimit.ι (pointwiseProduct F) ky' yk₀' = colimit.ι (pointwiseProduct F) k yk'
hy :
  colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk) =
    colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk')
k' : (s : α) → I s
f : (s : α) → k s ⟶ k' s
hk' :
  ∀ (s : α),
    (F s).map (f s) (Pi.π (fun s => (F s).obj (k s)) s yk) = (F s).map (f s) (Pi.π (fun s => (F s).obj (k s)) s yk')
⊢ (pointwiseProduct F).map f yk = (pointwiseProduct F).map f yk'

Tactic:
exact Types.limit_ext' _ _ _ (fun ⟨s⟩ => by simpa using hk' _)

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
yk' : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = colimit.ι (pointwiseProduct F) k yk
hyk₀' : colimit.ι (pointwiseProduct F) ky' yk₀' = colimit.ι (pointwiseProduct F) k yk'
hy :
  colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk) =
    colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk')
hch :
  ∀ (s : α),
    ∃ i' hi',
      (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk) = (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk')
⊢ colimit.ι (pointwiseProduct F) k yk = colimit.ι (pointwiseProduct F) k yk'

Tactic:
choose k' f hk' using hch

Result:
case refine_1.intro.intro.intro.intro
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
yk' : ∏ᶜ fun s => (F s).obj (k s) := (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = colimit.ι (pointwiseProduct F) k yk
hyk₀' : colimit.ι (pointwiseProduct F) ky' yk₀' = colimit.ι (pointwiseProduct F) k yk'
hy :
  colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk) =
    colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk')
k' : (s : α) → I s
f : (s : α) → k s ⟶ k' s
hk' :
  ∀ (s : α),
    (F s).map (f s) (Pi.π (fun s => (F s).obj (k s)) s yk) = (F s).map (f s) (Pi.π (fun s => (F s).obj (k s)) s yk')
⊢ colimit.ι (pointwiseProduct F) k yk = colimit.ι (pointwiseProduct F) k yk'

Proof state:
case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : ∏ᶜ fun s => colimit (F s)
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk : ∀ (s : α), colimit.ι (F s) (k s) (p s) = Pi.π (fun s => colimit (F s)) s x
x✝ : Discrete α
s : α
this :
  (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s => colimit (F s)) s)
      ((productIso fun s => (F s).obj (k s)).inv p) =
    (Pi.π (fun s => (F s).obj (k s)) s ≫ colimit.ι (F s) (k s)) ((productIso fun s => (F s).obj (k s)).inv p)
⊢ limit.π (Discrete.functor fun s => colimit (F s)) { as := s }
      (colimitPointwiseProductToProductColimit F
        (colimit.ι (pointwiseProduct F) k ((productIso fun s => (F s).obj (k s)).inv p))) =
    limit.π (Discrete.functor fun s => colimit (F s)) { as := s } x

Tactic:
exact this.trans (by simpa using hk _)

Result:
no goals