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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
ext
  simp [R.arrows.functorPushforward_comp F G]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P ⊤

Tactic:
rw [← arrows_top, ← generate_of_singleton_isSplitEpi (𝟙 X)]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (generate (singleton (𝟙 X))).arrows
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a.mk
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
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ unop Z
hf✝ : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop)))).arrows f✝
⊢ Multiequalizer.ι ((unop S).index P) ({ Y := Y✝, f := f✝, hf := hf✝ }.map e.inv).base =
    Multiequalizer.ι ((unop S).index P) { Y := Y✝, f := f✝, hf := hf✝ }.base.base

Tactic:
dsimp only [Cover.Arrow.base, Cover.Arrow.map]

Goal state after:
case e_a.mk
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
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ unop Z
hf✝ : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop)))).arrows f✝
⊢ Multiequalizer.ι ((unop S).index P) { Y := Y✝, f := f✝ ≫ g.unop ≫ f.unop, hf := ⋯ } =
    Multiequalizer.ι ((unop S).index P) { Y := Y✝, f := (f✝ ≫ g.unop) ≫ f.unop, hf := ⋯ }
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
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ IsIso (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))

Tactic:
· intro h
    refine ⟨IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ?_ ?_)⟩
    · apply (@asIso _ _ _ _ _ h).symm
    · intro a
      symm
      simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
⊢ IsSheafFor ((Over.map p).op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor P (ofArrows (fun i ↦ (Over.map p).obj (Y i)) fun i ↦ (Over.map p).map (f i))

Tactic:
let e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
      Subtype (Arrows.Compatible P (fun i ↦ (Over.map p).map (f i))) :=
    { toFun s := ⟨fun i ↦ s.val i, fun i₁ i₂ Z g₁ g₂ h ↦ by
        replace h := (Over.forget _).congr_map h
        dsimp at h
        have := s.property i₁ i₂ (Over.mk (g₁.left ≫ (f i₁).left ≫ X.hom))
          (Over.homMk g₁.left) (Over.homMk g₂.left (by
            have := Over.w (f i₂)
            dsimp at this ⊢
            rw [reassoc_of% h, this])) (by cat_disch)
        let φ : Z ⟶ (Over.map p).obj (Over.mk (g₁.left ≫ (f i₁).left ≫ X.hom)) :=
          Over.homMk (𝟙 _) (by simpa using Over.w g₁)
        replace this := congr_arg (P.map φ.op) this
        dsimp at this
        simp only [← comp_apply, ← Functor.map_comp, ← op_comp] at this
        convert! this <;> cat_disch⟩
      invFun s := ⟨fun i ↦ s.val i, fun i₁ i₂ Z g₁ g₂ h ↦
        s.property i₁ i₂ _ ((Over.map p).map g₁) ((Over.map p).map g₂)
          (by simp only [← Functor.map_comp, h])⟩ }

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
  Subtype (Arrows.Compatible P fun i ↦ (Over.map p).map (f i)) :=
  { toFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, invFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ IsSheafFor ((Over.map p).op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor P (ofArrows (fun i ↦ (Over.map p).obj (Y i)) fun i ↦ (Over.map p).map (f i))
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
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)
⊢ ∀ (I : (S.bind T).Relation),
    (ConcreteCategory.hom (P.map I.r.g₁.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) I.fst) =
      (ConcreteCategory.hom (P.map I.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) I.snd)

Tactic:
intro II

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
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)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom (P.map II.r.g₁.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst) =
    (ConcreteCategory.hom (P.map II.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd)
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)
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 := ⋯
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 := ⋯
I : S.Arrow
⊢ ∀ (I_1 : (T I).Arrow),
    (ConcreteCategory.hom ((J.plusObj P).map I_1.f.op)) (mk (w.pullback I.f)) =
      (ConcreteCategory.hom ((J.plusObj P).map I_1.f.op)) (mk (t I))

Tactic:
intro II

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)
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
⊢ (ConcreteCategory.hom ((J.plusObj P).map II.f.op)) (mk (w.pullback I.f)) =
    (ConcreteCategory.hom ((J.plusObj P).map II.f.op)) (mk (t I))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).fst =
    S.fst

pp: case property.refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).snd =
    S.snd

pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }

Tactic:
· delta pullbackCone
        ext a
        dsimp

Goal state after:
case property.refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).snd =
    S.snd

case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).snd =
    S.snd

pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }

Tactic:
· delta pullbackCone
        ext a
        dsimp

Goal state after:
case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }

Tactic:
intro m h₁ h₂

Goal state after:
case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
⊢ m =
    ofHom
      { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
      ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩) =
    x

Tactic:
apply Concrete.limit_ext

Goal state after:
case h
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ ∀ (j : Discrete WalkingPair),
    (ConcreteCategory.hom (limit.π (pair X Y) j))
        ((ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
          ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩)) =
      (ConcreteCategory.hom (limit.π (pair X Y) j)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : ↑(W ⨯ X)
⊢ True ∧ True

Tactic:
and_self_iff

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

Goal state before:
pp: case h
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 (prod.map f g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂)) = x

Tactic:
apply Concrete.limit_ext

Goal state after:
case h
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
⊢ ∀ (j : Discrete WalkingPair),
    (ConcreteCategory.hom (limit.π (pair Y Z) j))
        ((ConcreteCategory.hom (prod.map f g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂))) =
      (ConcreteCategory.hom (limit.π (pair Y Z) j)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
      ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩) =
    x✝

Tactic:
apply Concrete.limit_ext

Goal state after:
case h
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ ∀ (j : WalkingCospan),
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) j))
        ((ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
          ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩)) =
      (ConcreteCategory.hom (limit.π (cospan g₁ g₂) j)) x✝
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr.refine_1
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩ ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U

Tactic:
simp only [coe_of, Set.mem_preimage]
      convert! hy
      rw [pullbackIsoProdSubtype_inv_snd_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ IsVanKampenColimit c

Tactic:
have : F = pair X Y := by
    apply Functor.hext
    · rintro ⟨⟨⟩⟩ <;> rfl
    · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X, Y]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
this : F = pair X Y
⊢ IsVanKampenColimit 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₀
⊢ FinitaryExtensive C ↔ IsVanKampenColimit c₀

Tactic:
refine ⟨fun H => H.van_kampen' c₀ hc₀, fun H => ?_⟩

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 : IsVanKampenColimit c₀
⊢ FinitaryExtensive C
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
y : (j : J) → F.obj (j, k j) := fun j ↦ ⋯.choose
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x

Tactic:
have e : ∀ j,
        colimit.ι ((curry.obj F).obj j) (k j) (y j) = limit.π (curry.obj F ⋙ Limits.colim) j x :=
      fun j => (z j).choose_spec.choose_spec

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
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₂.uniq
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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))) (m : Z ⟶ s.pt),
    (↾fun p ↦ (↑p).1) ≫ m = s.inl →
      (↾fun p ↦ (↑p).1) ≫ m = s.inr →
        m =
          ↾fun x ↦
            if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
            else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)

Tactic:
· intro s m e₁ e₂
      ext x
      simp only [TypeCat.Fun.toFun_apply, Types.binaryCoproductCocone_pt, pair_obj_left,
        Functor.const_obj_obj, pair_obj_right, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
      split_ifs
      · rw [← e₁]
        rfl
      · rw [← e₂]
        rfl

Goal state after: