-- 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')
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')

Tactic:
have hy₁ := congrFun (ι_colimitPointwiseProductToProductColimit_π F k s) yk

Result:
α : 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')
s : α
hy₁ :
  (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s => colimit (F s)) s) yk =
    (Pi.π (fun s => (F s).obj (k s)) s ≫ colimit.ι (F s) (k s)) yk
⊢ ∃ 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')

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')
s : α
hy₁ :
  Pi.π (fun s => colimit (F s)) s (colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk)) =
    colimit.ι (F s) (k s) (Pi.π (fun s => (F s).obj (k s)) s yk)
hy₂ :
  Pi.π (fun s => colimit (F s)) s (colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk')) =
    colimit.ι (F s) (k s) (Pi.π (fun s => (F s).obj (k s)) s yk')
⊢ ∃ 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')

Tactic:
rw [← hy, hy₁, Types.FilteredColimit.colimit_eq_iff] at hy₂

Result:
α : 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')
s : α
hy₁ :
  Pi.π (fun s => colimit (F s)) s (colimitPointwiseProductToProductColimit F (colimit.ι (pointwiseProduct F) k yk)) =
    colimit.ι (F s) (k s) (Pi.π (fun s => (F s).obj (k s)) s yk)
hy₂ :
  ∃ k_1 f g, (F s).map f (Pi.π (fun s => (F s).obj (k s)) s yk) = (F s).map g (Pi.π (fun s => (F s).obj (k s)) s yk')
⊢ ∃ 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')

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
y y' : colimit (pointwiseProduct F)
hy : colimitPointwiseProductToProductColimit F y = colimitPointwiseProductToProductColimit F y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = y
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
hyk₀' : colimit.ι (pointwiseProduct F) ky' yk₀' = y'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : (pointwiseProduct F).obj k := (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
⊢ y = y'

Tactic:
let yk' : (pointwiseProduct F).obj k :=
  (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'

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
y y' : colimit (pointwiseProduct F)
hy : colimitPointwiseProductToProductColimit F y = colimitPointwiseProductToProductColimit F y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = y
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
hyk₀' : colimit.ι (pointwiseProduct F) ky' yk₀' = y'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : (pointwiseProduct F).obj k := (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
yk' : (pointwiseProduct F).obj k := (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
⊢ y = y'

Proof state:
case refine_1.intro.intro
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : colimit (pointwiseProduct F)
hy : colimitPointwiseProductToProductColimit F y = colimitPointwiseProductToProductColimit F y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = y
⊢ y = y'

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

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
y y' : colimit (pointwiseProduct F)
hy : colimitPointwiseProductToProductColimit F y = colimitPointwiseProductToProductColimit F y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : colimit.ι (pointwiseProduct F) ky yk₀ = y
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
hyk₀' : colimit.ι (pointwiseProduct F) ky' yk₀' = y'
⊢ y = y'