mathlib-initiative/mathlib-tactics huggingface dataset:
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := S.bind T
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := meqOfSep P hsep X S s T t ht
I : S.Arrow
II : (T I).Arrow
Y : C
⊢ ∀ (f : Y ⟶ II.Y),
    (↑((J.pullback II.f).obj (T I))).arrows f → (↑((J.pullback II.f).obj ((J.pullback I.f).obj B))).arrows f

Tactic:
f

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := S.bind T
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := meqOfSep P hsep X S s T t ht
I : S.Arrow
II : (T I).Arrow
Y : C
f : Y ⟶ II.Y
⊢ (↑((J.pullback II.f).obj (T I))).arrows f → (↑((J.pullback II.f).obj ((J.pullback I.f).obj B))).arrows f
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k k' : K
⊢ ∀ (f : k ⟶ k'),
    (curry.obj (swap K J ⋙ F) ⋙ lim).map f ≫
        limit.π ((curry.obj (swap K J ⋙ F)).obj k') j ≫ colimit.ι ((curry.obj F).obj j) k' =
      (limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) ≫
        ((const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f

Tactic:
f

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k k' : K
f : k ⟶ k'
⊢ (curry.obj (swap K J ⋙ F) ⋙ lim).map f ≫
      limit.π ((curry.obj (swap K J ⋙ F)).obj k') j ≫ colimit.ι ((curry.obj F).obj j) k' =
    (limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) ≫
      ((const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
⊢ ∀ (f : j ⟶ j'),
    ((const J).obj (colimit.cocone (curry.obj (swap K J ⋙ F) ⋙ lim)).1).map f ≫
        colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj j')).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k,
                naturality := ⋯ } } =
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj j)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                naturality := ⋯ } } ≫
        (curry.obj F ⋙ colim).map f

Tactic:
f

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
⊢ ((const J).obj (colimit.cocone (curry.obj (swap K J ⋙ F) ⋙ lim)).1).map f ≫
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
        { pt := (colimit.cocone ((curry.obj F).obj j')).1,
          ι :=
            { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k,
              naturality := ⋯ } } =
    colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
        { pt := (colimit.cocone ((curry.obj F).obj j)).1,
          ι :=
            { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
              naturality := ⋯ } } ≫
      (curry.obj F ⋙ colim).map f
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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
⊢ ∀ (f : i ⟶ j),
    ((Functor.const K).obj S.pt).map f ≫
        (Presheaf.isLimitOfIsSheaf J (F.obj j).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj j).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app j).app (op i.Y)) ⋯) =
      (Presheaf.isLimitOfIsSheaf J (F.obj i).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj i).obj) S.pt (fun i_1 ↦ S.ι i_1 ≫ (E.π.app i).app (op i_1.Y)) ⋯) ≫
        (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f

Tactic:
f

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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
⊢ ((Functor.const K).obj S.pt).map f ≫
      (Presheaf.isLimitOfIsSheaf J (F.obj j).obj W ⋯).lift
        (Multifork.ofι (W.index (F.obj j).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app j).app (op i.Y)) ⋯) =
    (Presheaf.isLimitOfIsSheaf J (F.obj i).obj W ⋯).lift
        (Multifork.ofι (W.index (F.obj i).obj) S.pt (fun i_1 ↦ S.ι i_1 ≫ (E.π.app i).app (op i_1.Y)) ⋯) ≫
      (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
iSup_le_iff

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) =
    {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

Tactic:
ext x
  constructor
  · rintro ⟨y, rfl⟩
    simp only [← ConcreteCategory.comp_apply, Set.mem_ofPred_eq]
    simp [pullback.condition]
  · rintro (h : f (_, _).1 = g (_, _).2)
    use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩
    apply Concrete.limit_ext
    rintro ⟨⟨⟩⟩ <;>
      rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π] <;>
      -- This used to be `simp` before https://github.com/leanprover/lean4/pull/2644
      cat_disch

Goal state after:
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 (pullback.fst g₁ g₂ ≫ g₁)) x✝ =
    (ConcreteCategory.hom g₂) ((ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝)

Tactic:
pullback.condition,

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 (pullback.snd g₁ g₂ ≫ g₂)) x✝ =
    (ConcreteCategory.hom g₂) ((ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty.{1} ⥤ C
c' : Cocone F'
α : F' ⟶ empty C
⊢ ∀ (f : c'.pt ⟶ (asEmptyCocone X).pt),
    α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f →
      NatTrans.Equifibered α →
        (Nonempty (IsColimit c') ↔
          ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j))

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty.{1} ⥤ C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
⊢ α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f →
    NatTrans.Equifibered α →
      (Nonempty (IsColimit c') ↔
        ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j))
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 : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
⊢ ∀ (f : c''.pt ⟶ c'.pt),
    α ≫ c'.ι = c''.ι ≫ (const J).map f →
      NatTrans.Equifibered α → (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)) → Nonempty (IsColimit c'')

Tactic:
f

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
⊢ α ≫ c'.ι = c''.ι ≫ (const J).map f →
    NatTrans.Equifibered α → (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)) → Nonempty (IsColimit c'')
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_1
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
⊢ (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)

Tactic:
f

Goal state after:
case mpr.refine_1
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
f : X ⟶ T
⊢ (Y ⟶ T) → (c.pt ⟶ T)
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 : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
⊢ ∀ (f : c''.pt ⟶ c'.pt),
    α ≫ c'.ι = c''.ι ≫ (const J).map f →
      NatTrans.Equifibered α → (Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j))

Tactic:
f

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
⊢ α ≫ c'.ι = c''.ι ≫ (const J).map f →
    NatTrans.Equifibered α → (Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j))
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 : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
⊢ ∀ (f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt),
    α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f →
      NatTrans.Equifibered α' →
        (Nonempty (IsColimit c') ↔
          ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j))

Tactic:
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 : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
⊢ α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f →
    NatTrans.Equifibered α' →
      (Nonempty (IsColimit c') ↔
        ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j))
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),
    α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f →
      NatTrans.Equifibered α' →
        (∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)) →
          Nonempty (IsColimit c')

Tactic:
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
⊢ α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f →
    NatTrans.Equifibered α' →
      (∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)) →
        Nonempty (IsColimit c')
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
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝⁴ : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst✝³ : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst✝² : ReflectsLimitsOfShape WalkingCospan G
inst✝¹ : PreservesColimitsOfShape J G
inst✝ : ReflectsColimitsOfShape J G
H : IsVanKampenColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
⊢ ∀ (f : c'.pt ⟶ c.pt),
    α ≫ c.ι = c'.ι ≫ (const J).map f →
      NatTrans.Equifibered α → (Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j))

Tactic:
f

Goal state after:
J : Type v'
inst✝⁷ : Category.{u', v'} J
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝⁴ : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst✝³ : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst✝² : ReflectsLimitsOfShape WalkingCospan G
inst✝¹ : PreservesColimitsOfShape J G
inst✝ : ReflectsColimitsOfShape J G
H : IsVanKampenColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
⊢ α ≫ c.ι = c'.ι ≫ (const J).map f →
    NatTrans.Equifibered α → (Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_2
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
⊢ ∀ (f : X ⟶ T) (g : Y ⟶ T),
    c.inl ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      f

Tactic:
f

Goal state after:
case mpr.refine_2
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
f : X ⟶ T
⊢ ∀ (g : Y ⟶ T),
    c.inl ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      f
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
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),
    α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f →
      NatTrans.Equifibered α →
        (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)) →
          Nonempty (IsColimit c')

Tactic:
f

Goal state after:
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
⊢ α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f →
    NatTrans.Equifibered α →
      (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)) → Nonempty (IsColimit c')
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_3
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
⊢ ∀ (f : X ⟶ T) (g : Y ⟶ T),
    c.inr ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      g

Tactic:
f

Goal state after:
case mpr.refine_3
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
f : X ⟶ T
⊢ ∀ (g : Y ⟶ T),
    c.inr ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      g
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k ↦ X ↑k
hc₂ : IsColimit c₂
⊢ Mono (Cofan.IsColimit.desc hc₁ fun i ↦ c.inj (ι i))

Tactic:
by
  classical
  let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)
  refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
    hc₁ hc₂ _ (by simp [e])
  exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocone.equivalenceOfReindexing
    (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocone.ext (Iso.refl _))

Goal state after:
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
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),
    α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f →
      NatTrans.Equifibered α →
        (Nonempty (IsColimit c') ↔
          ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j))

Tactic:
f

Goal state after:
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
⊢ α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f →
    NatTrans.Equifibered α →
      (Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j))