mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case right.e_a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b)) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b))

Tactic:
apply hP.amalgamate_map

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op = E.π.app (WalkingMulticospan.left I)

Tactic:
apply hP.amalgamate_map

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    (J.plusObj P).map f ≫ colimMap (J.diagramNatTrans η (unop Y)) =
      colimMap (J.diagramNatTrans η (unop X)) ≫ (J.plusObj Q).map f

Tactic:
by
    intro X Y f
    dsimp [plusObj]
    ext
    simp only [diagramPullback_app, ι_colimMap, colimit.ι_pre_assoc, colimit.ι_pre,
      ι_colimMap_assoc, Category.assoc]
    simp_rw [← Category.assoc]
    congr 1
    exact Multiequalizer.hom_ext _ _ _ (fun I => by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          colimit.ι (J.diagram P I.Y) (op ⊤)))
      (↑x I) =
    (ConcreteCategory.hom
        (colimMap (J.diagramPullback P I.f.op.unop) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op))
      (mk x)

Tactic:
dsimp [mk]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          colimit.ι (J.diagram P I.Y) (op ⊤)))
      (↑x I) =
    (ConcreteCategory.hom (colimMap (J.diagramPullback P I.f) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f).op))
      ((ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm x))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = mk ((Meq.equiv P (unop S)) y)

Tactic:
dsimp [mk]

Goal state after:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) ((Meq.equiv P (unop S)).symm ((Meq.equiv P (unop S)) y))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })
⊢ ((parallelPair (s.map (firstMap R P)) (s.map (secondMap R P))).map WalkingParallelPairHom.right ≫
        (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))).hom) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j =
    ((PreservesProduct.iso s fun f ↦ P.obj (op f.fst)).hom ≫
        (parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R)).map
          WalkingParallelPairHom.right) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j

Tactic:
dsimp [Equalizer.Presieve.secondMap, secondMap]

Goal state after:
case refine_2
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })
⊢ (s.map (Pi.lift fun x ↦ Pi.π (fun f ↦ P.obj (op f.fst)) x.2 ≫ P.map (pullback.snd ↑x.1.snd ↑x.2.snd).op) ≫
        piComparison s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ≫
      limit.π (Discrete.functor fun fg ↦ s.obj (P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))) j =
    ((piComparison s fun f ↦ P.obj (op f.fst)) ≫
        Pi.lift fun fg ↦
          Pi.π (fun f ↦ s.obj (P.obj (op f.fst))) fg.2 ≫ s.map (P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)) ≫
      limit.π (Discrete.functor fun fg ↦ s.obj (P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))) j
Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.plusFunctor D ⋙ (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.plusFunctor E ≅
    ((whiskeringRight Cᵒᵖ D E).obj F ⋙ J.plusFunctor E) ⋙ J.plusFunctor E

Tactic:
refine (associator _ _ _).symm ≪≫ ?_

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ (J.plusFunctor D ⋙ (whiskeringRight Cᵒᵖ D E).obj F) ⋙ J.plusFunctor E ≅
    ((whiskeringRight Cᵒᵖ D E).obj F ⋙ J.plusFunctor E) ⋙ J.plusFunctor E
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
      { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) } =
    S.ι.app j

Tactic:
by ext1; dsimp; rw [hE.fac]; rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)

Tactic:
intro
    apply Functor.map_epi

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
by
  let c' := coconeOfCoconeForget ((forget).mapCocone c)
  let hc' : IsColimit c' := isColimitCoconeOfForget _ (isColimitOfPreserves forget hc)
  let e := IsColimit.coconePointUniqueUpToIso hc' hc
  have he (j : J) : c'.ι.app j ≫ e.hom = c.ι.app j :=
    IsColimit.comp_coconePointUniqueUpToIso_hom hc' hc j
  apply (homeoOfIso e).coinduced_eq.symm.trans
  dsimp [coconeOfCoconeForget_pt, c', topologicalSpaceCoconePtOfCoconeForget]
  simp only [coinduced_iSup]
  conv_rhs => simp only [← he]
  rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ ofHom { toFun := fun x ↦ (↑x).1, continuous_toFun := ⋯ } ≫ f =
    ofHom { toFun := fun x ↦ (↑x).2, continuous_toFun := ⋯ } ≫ g

Tactic:
ext ⟨x, h⟩

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑X × ↑Y
h : (ConcreteCategory.hom f) x.1 = (ConcreteCategory.hom g) x.2
⊢ (ConcreteCategory.hom (ofHom { toFun := fun x ↦ (↑x).1, continuous_toFun := ⋯ } ≫ f)) ⟨x, h⟩ =
    (ConcreteCategory.hom (ofHom { toFun := fun x ↦ (↑x).2, continuous_toFun := ⋯ } ≫ g)) ⟨x, h⟩
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case h.left
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom prod.fst) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂))) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x

Tactic:
TopCat.prodIsoProd_inv_fst_apply

Goal state after:
case h.left
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom f) (x₁, x₂).1 = (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inl

pp: case refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inr

pp: case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr →
        m =
          ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }

Tactic:
· intro s
    ext
    rfl

Goal state after:
case refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inr

case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr →
        m =
          ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
        ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inr

pp: case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr →
        m =
          ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }

Tactic:
· intro s
    ext
    rfl

Goal state after:
case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr →
        m =
          ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ IsQuotientMap ⇑(ConcreteCategory.hom c.π)

Tactic:
isQuotientMap_iff

Goal state after:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ IsCoinducing ⇑(ConcreteCategory.hom c.π) ∧ Function.Surjective ⇑(ConcreteCategory.hom c.π)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' : C
⊢ ∀ {Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

Tactic:
Y'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
⊢ ∀ (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
z :
  ∀ (j : J),
    ∃ j_1 y,
      (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) j_1)) y =
        (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k : J → K := fun j ↦ ⋯.choose
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x

Tactic:
let y : ∀ j, F.obj (j, k j) := fun j => (z j).choose_spec.choose

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
z :
  ∀ (j : J),
    ∃ j_1 y,
      (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) j_1)) y =
        (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k : J → K := fun j ↦ ⋯.choose
y : (j : J) → F.obj (j, k j) := fun j ↦ ⋯.choose
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' : C
⊢ ∀ ⦃Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

Tactic:
Y'

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' : C
⊢ ∀ ⦃Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' : C
⊢ ∀ ⦃Y' Z' : C⦄ (f' : W' ⟶ X') (g' : W' ⟶ Y') (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αW : W' ⟶ W) (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (αZ : Z' ⟶ Z),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)

Tactic:
Y'

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' : C
⊢ ∀ ⦃Z' : C⦄ (f' : W' ⟶ X') (g' : W' ⟶ Y') (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αW : W' ⟶ W) (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (αZ : Z' ⟶ Z),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' : TopCat
⊢ ∀ {Y' : TopCat} (αX : X' ⟶ TopCat.of PUnit.{u + 1}) (αY : Y' ⟶ TopCat.of PUnit.{u + 1})
    (f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt),
    αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f →
      αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f →
        IsPullback (X'.binaryCofan Y').inl αX f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl ∧
          IsPullback (X'.binaryCofan Y').inr αY f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr

Tactic:
Y'

Goal state after:
case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
⊢ ∀ (αX : X' ⟶ TopCat.of PUnit.{u + 1}) (αY : Y' ⟶ TopCat.of PUnit.{u + 1})
    (f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt),
    αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f →
      αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f →
        IsPullback (X'.binaryCofan Y').inl αX f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl ∧
          IsPullback (X'.binaryCofan Y').inr αY f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.isoClosure.isLocal f → P.isLocal f

Tactic:
intro hf Z hZ
    exact hf _ (P.le_isoClosure _ hZ)

Goal state after: