-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
lemma isIso_f [IsFiltered J] : IsIso (f z)

Proof state:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
      ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
ext j

Result:
case refine_1.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫
      colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
        ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Proof state:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ (Iso.refl (Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z)))).left).hom ≫ (Arrow.mk (f z)).hom =
    (Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z)))).hom ≫
      ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
dsimp

Result:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
      ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Proof state:
case refine_1.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z = (pullback.snd c.ι ((Functor.const J).map z)).app j

Tactic:
apply hf

Result:
no goals

Proof state:
case refine_1.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫
      colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
        ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
rw [Category.id_comp, ι_colimMap_assoc, colimit.comp_coconePointUniqueUpToIso_hom,
  constCocone_ι, NatTrans.id_app, Category.comp_id]

Result:
case refine_1.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z = (pullback.snd c.ι ((Functor.const J).map z)).app j

Proof state:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ Arrow.mk (colim.map c.ι) ≅ Arrow.mk (𝟙 c.pt)

Tactic:
exact Arrow.isoMk (IsColimit.coconePointUniqueUpToIso (colimit.isColimit Y) hc)
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
    (isColimitConstCocone J c.pt))

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z))) ≅ Arrow.mk (f z)

Tactic:
refine Arrow.isoMk (Iso.refl _)
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (isColimitConstCocone J X)) ?_

Result:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ (Iso.refl (Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z)))).left).hom ≫ (Arrow.mk (f z)).hom =
    (Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z)))).hom ≫
      ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Proof state:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ MorphismProperty.isomorphisms C (colim.map c.ι)

Tactic:
refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).2
  (inferInstanceAs (IsIso (𝟙 c.pt)))

Result:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ Arrow.mk (colim.map c.ι) ≅ Arrow.mk (𝟙 c.pt)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ IsIso (f z)

Tactic:
refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).1
  (MorphismProperty.of_isPullback
    ((IsPullback.of_hasPullback c.ι ((Functor.const _).map z)).map colim) ?_)

Result:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z))) ≅ Arrow.mk (f z)

case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ MorphismProperty.isomorphisms C (colim.map c.ι)