mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
⊢ (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X) ≫ (F.obj k).obj.map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
← Category.assoc

Goal state after:
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✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
⊢ ((isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
        (E.π.app k).app (op X)) ≫
      (F.obj k).obj.map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
X Y : J
f : X ⟶ Y
a : ↑(((Functor.const J).obj (of ↑{u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j})).obj X)
⊢ (ConcreteCategory.hom
        (((Functor.const J).obj (of ↑{u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j})).map
            f ≫
          ofHom { toFun := fun u ↦ ↑u Y, continuous_toFun := ⋯ }))
      a =
    (ConcreteCategory.hom (ofHom { toFun := fun u ↦ ↑u X, continuous_toFun := ⋯ } ≫ F.map f)) a

Tactic:
exact (a.2 f).symm

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
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i✝)) x) = (ConcreteCategory.hom (S.π.app j✝)) x

Tactic:
← S.w f

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i✝)) x) =
    (ConcreteCategory.hom (S.π.app i✝ ≫ F.map f)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i)) x) = (ConcreteCategory.hom (S.π.app j)) x

Tactic:
← S.w f

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i)) x) =
    (ConcreteCategory.hom (S.π.app i ≫ F.map f)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom g₁) ((ConcreteCategory.hom i₁) x₁) = (ConcreteCategory.hom g₂) ((ConcreteCategory.hom i₂) x₂)

Tactic:
hx₁,

Goal state after:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom g₁) ((ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝) =
    (ConcreteCategory.hom g₂) ((ConcreteCategory.hom i₂) x₂)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: case intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
x y : colimit (curry.obj (swap K J ⋙ F) ⋙ lim)
h : (ConcreteCategory.hom (colimitLimitToLimitColimit F)) x = (ConcreteCategory.hom (colimitLimitToLimitColimit F)) y
⊢ x = y

Tactic:
obtain ⟨kx, x, rfl⟩ := jointly_surjective' x

Goal state after:
case intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
y : colimit (curry.obj (swap K J ⋙ F) ⋙ lim)
kx : K
x : (curry.obj (swap K J ⋙ F) ⋙ lim).obj kx
h :
  (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x) =
    (ConcreteCategory.hom (colimitLimitToLimitColimit F)) y
⊢ (ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x = y
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α'
H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j)

Tactic:
← Category.comp_id f

Goal state after:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α'
H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) (f ≫ 𝟙 ((Cocone.precompose α).obj c).pt) (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k) f
    (c.ι.app k)

Tactic:
← Category.comp_id f

Goal state after:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k)
    (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)

Tactic:
refine .of_iso_pullback (by simp) ?_ ?_ ?_
  · refine hY.uniqueUpToIso ?_
    exact IsInitial.ofCoproductDisjointOfIsColimit hij hc
  · simp
  · simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case e'_2.mp
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
k : K
⊢ IsPullback (c'.ι.app (e.inverse.obj k)) (α.app (e.inverse.obj k) ≫ F.map (e.counit.app k)) f (c.ι.app k)

Tactic:
← Category.comp_id f

Goal state after:
case e'_2.mp
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
k : K
⊢ IsPullback (c'.ι.app (e.inverse.obj k)) (α.app (e.inverse.obj k) ≫ F.map (e.counit.app k))
    (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_4
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
m : c.pt ⟶ T
x : ↑c.pt
⊢ (ConcreteCategory.hom m) x =
    if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
      (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
    else (ConcreteCategory.hom (c.inr ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)

Tactic:
split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_1
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)

Tactic:
rw [(IsColimit.equivOfNatIsoOfIso (diagramIsoSpan F') c' (PushoutCocone.mk _ _ this)
            _).nonempty_congr]

Goal state after:
case mp.refine_1
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)

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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_1.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ c.inr ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
← Category.assoc

Goal state after:
case mp.refine_1.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl

Tactic:
have : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y) := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this✝ : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
⊢ ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
Module: Mathlib.CategoryTheory.ObjectProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : W.isColocal.colimitsOfShape J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : W.isColocal.ColimitOfShape J X
f : X ⟶ Z
app : (j : J) → p.diag.obj j ⟶ Y
h : ∀ (j : J), (fun f ↦ f ≫ g) (app j) = p.ι.app j ≫ f
⊢ ∃ a, (fun f ↦ f ≫ g) a = f

Tactic:
exact ⟨p.isColimit.desc (Cocone.mk _
      { app := app
        naturality _ _ a := (p.prop_diag_obj _ g hg).1
          (by simp [h]) }),
      p.isColimit.hom_ext (fun j ↦ by simp [p.isColimit.fac_assoc, h])⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map
        (L₁.map (adj.unit.app X₁) ≫
          (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ (CatCommSq.iso F L₂ L₁ F').inv.app (G.obj X₁)) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj (G.obj X₁)) ≫
        L₂.map (adj.counit.app (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map (L₁.map (adj.unit.app X₁) ≫ 𝟙 ((F ⋙ L₁).obj (G.obj X₁))) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj (G.obj X₁)) ≫
        L₂.map (adj.counit.app (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mp.mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)

Tactic:
· rintro H ⟨⟨⟩⟩
      exacts [H.1, H.2]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      L₁.map (adj.unit.app (F.obj X₂)) ≫
        (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj (F.obj X₂)) ≫
          F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app (F.obj X₂) ≫ (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫
            F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      L₁.map (adj.unit.app (F.obj X₂)) ≫
        (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj (F.obj X₂)) ≫
          F'.map (𝟙 ((G ⋙ L₂).obj (F.obj X₂))) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mpr.mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {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)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

pp: case mpr.mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {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)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) →
    IsPullback c'.inl (α.app { as := WalkingPair.left })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr

Tactic:
· rintro H ⟨⟨⟩⟩
      exacts [H.1, H.2]

Goal state after:
case mpr.mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {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)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) →
    IsPullback c'.inl (α.app { as := WalkingPair.left })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
⊢ P ≤ P.isColocal.isColocal

Tactic:
rw [← le_isColocal_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsPullback (initial.to ((pair X Y).obj { as := WalkingPair.left }))
    (initial.to ((pair X Y).obj { as := WalkingPair.right })) c.inl c.inr

Tactic:
refine ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.left⟩).flip

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))