mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced ((Prod.fst ∘ Subtype.val) ∘ ⇑homeo) X.str ⊓ induced ((Prod.snd ∘ Subtype.val) ∘ ⇑homeo) Y.str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Tactic:
rfl

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

Goal state before:
pp: case right
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
x✝ : ↑S.pt
⊢ (ConcreteCategory.hom
        (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ } ≫
          (X.prodBinaryFan Y).π.app { as := WalkingPair.right }))
      x✝ =
    (ConcreteCategory.hom (S.π.app { as := WalkingPair.right })) x✝

Tactic:
rfl

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

Goal state before:
pp: X Y : TopCat
⊢ prodFst = (X.prodBinaryFan Y).π.app { as := WalkingPair.left }

Tactic:
rfl

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

Goal state before:
pp: X Y : TopCat
⊢ prodSnd = (X.prodBinaryFan Y).π.app { as := WalkingPair.right }

Tactic:
rfl

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

Goal state before:
pp: X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (Prod.fst ∘ ⇑homeo) X.str ⊓ induced (Prod.snd ∘ ⇑homeo) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Tactic:
rfl

Goal state after:
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
x✝ : ↑X
⊢ (ConcreteCategory.hom
        (ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
          ofHom
            { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }))
      x✝ =
    (ConcreteCategory.hom s.inl) x✝

Tactic:
rfl

Goal state after:
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
x✝ : ↑Y
⊢ (ConcreteCategory.hom
        (ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
          ofHom
            { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }))
      x✝ =
    (ConcreteCategory.hom s.inr) x✝

Tactic:
rfl

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

Goal state before:
pp: case e'_5
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) =
    ⇑(ConcreteCategory.hom (pullback.snd f g ≫ g))

Tactic:
rfl

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

Goal state before:
pp: case e'_5
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) =
    ⇑(ConcreteCategory.hom (pullback.snd f g ≫ g))

Tactic:
rfl

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

Goal state before:
pp: case neg
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
⊢ Continuous
    ((range ⇑(ConcreteCategory.hom c.inl))ᶜ.domRestrict fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))

Tactic:
have : ∀ a, a ∉ Set.range c.inl → a ∈ Set.range c.inr := by
              rintro a (h : a ∈ (Set.range c.inl)ᶜ)
              rwa [eq_compl_iff_isCompl.mpr h₃.symm]

Goal state after:
case neg
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
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous
    ((range ⇑(ConcreteCategory.hom c.inl))ᶜ.domRestrict fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
⊢ ((BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl ≫
      ↾fun x ↦ Sum.casesOn x (fun x ↦ (ConcreteCategory.hom f₁) x) fun x ↦ (ConcreteCategory.hom f₂) x) =
    f₁

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
⊢ ((BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inr ≫
      ↾fun x ↦ Sum.casesOn x (fun x ↦ (ConcreteCategory.hom f₁) x) fun x ↦ (ConcreteCategory.hom f₂) x) =
    f₂

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_obj.left
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 }
⊢ F.obj { as := WalkingPair.left } = (pair X Y).obj { as := WalkingPair.left }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_obj.right
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 }
⊢ F.obj { as := WalkingPair.right } = (pair X Y).obj { as := WalkingPair.right }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case fst
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
x✝ : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 }
⊢ (↑((fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩) ((fun p ↦ ⟨(↑p).1, ⋯⟩) x✝))).1 = (↑x✝).1

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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
x✝ : { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit }
⊢ ↑((fun p ↦ ⟨(↑p).1, ⋯⟩) ((fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩) x✝)) = ↑x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case fst
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 } := ⋯
x✝ : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 }
⊢ (↑((fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩) ((fun p ↦ ⟨(↑p).1, ⋯⟩) x✝))).1 = (↑x✝).1

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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 } := ⋯
x✝ : { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit }
⊢ ↑((fun p ↦ ⟨(↑p).1, ⋯⟩) ((fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩) x✝)) = ↑x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case neg
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 } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
x : Z
hx : (ConcreteCategory.hom f) (x, PUnit.unit).1 = (ConcreteCategory.hom (↾Sum.inr)) (x, PUnit.unit).2
h : ¬(ConcreteCategory.hom f) x = Sum.inl PUnit.unit
⊢ (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩) = (ConcreteCategory.hom s.inr) ⟨(x, PUnit.unit), hx⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case pos
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 } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
m : Z ⟶ s.pt
e₁ : (↾fun p ↦ (↑p).1) ≫ m = s.inl
e₂ : (↾fun p ↦ (↑p).1) ≫ m = s.inr
x : Z
h✝ : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit
⊢ (ConcreteCategory.hom m) x = (ConcreteCategory.hom ((↾fun p ↦ (↑p).1) ≫ m)) (eX.symm ⟨x, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case neg
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 } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
m : Z ⟶ s.pt
e₁ : (↾fun p ↦ (↑p).1) ≫ m = s.inl
e₂ : (↾fun p ↦ (↑p).1) ≫ m = s.inr
x : Z
h✝ : ¬(ConcreteCategory.hom f) x = Sum.inl PUnit.unit
⊢ (ConcreteCategory.hom m) x = (ConcreteCategory.hom ((↾fun p ↦ (↑p).1) ≫ m)) (eY.symm ⟨x, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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
⊢ FinitaryExtensive (Type u)

Tactic:
rw [finitaryExtensive_iff_of_isTerminal (Type u) PUnit Types.isTerminalPUnit _
      (Types.binaryCoproductColimit _ _)]
  apply BinaryCofan.isVanKampen_mk _ _ (fun X Y => Types.binaryCoproductColimit X Y) _
      fun f g => (Limits.Types.pullbackLimitCone f g).2
  · intro _ _ _ _ f hαX hαY
    constructor
    · refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · simp
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨↾(l), ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩
      · ext x
        exact (hl x).symm
      · ext x
        exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm
    · refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · simp
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨↾l, ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩
      · ext x
        exact (hl x).symm
      · ext x
        exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm
  · intro Z f
    dsimp [Limits.Types.binaryCoproductCocone]
    have : ∀ x, f x = Sum.inl PUnit.unit ∨ f x = Sum.inr PUnit.unit := by
      intro x
      rcases f x with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
      exacts [Or.inl rfl, Or.inr rfl]
    let eX : { p : Z × PUnit // f p.fst = Sum.inl p.snd } ≃ { x : Z // f x = Sum.inl PUnit.unit } :=
      ⟨fun p => ⟨p.1.1, by convert! p.2⟩, fun x => ⟨⟨_, _⟩, x.2⟩, fun _ => by ext; rfl,
        fun _ => by ext; rfl⟩
    let eY : { p : Z × PUnit // f p.fst = Sum.inr p.snd } ≃ { x : Z // f x = Sum.inr PUnit.unit } :=
      ⟨fun p => ⟨p.1.1, p.2.trans (congr_arg Sum.inr <| Subsingleton.elim _ _)⟩,
        fun x => ⟨⟨_, _⟩, x.2⟩, fun _ => by ext; rfl, fun _ => by ext; rfl⟩
    fapply BinaryCofan.isColimitMk
    · exact fun s => ↾fun x => dite _ (fun h => s.inl <| eX.symm ⟨x, h⟩)
        fun h => s.inr <| eY.symm ⟨x, (this x).resolve_left h⟩
    · intro s
      ext ⟨⟨x, ⟨⟩⟩, _⟩
      dsimp
      split_ifs with h <;> tauto
    · intro s
      ext ⟨⟨x, ⟨⟩⟩, hx⟩
      dsimp
      split_ifs with h
      · cases h.symm.trans hx
      · rfl
    · 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:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case fac_left
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 : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = s.inl

Tactic:
rfl

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

Goal state before:
pp: case mpr.uniq.h₁.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 : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ f ≫ s.inr = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_obj.left
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
⊢ (pair X Y ⋙ Gr).obj { as := WalkingPair.left } = (pair (Gr.obj X) (Gr.obj Y)).obj { as := WalkingPair.left }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_obj.right
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
⊢ (pair X Y ⋙ Gr).obj { as := WalkingPair.right } = (pair (Gr.obj X) (Gr.obj Y)).obj { as := WalkingPair.right }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case refine_2
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
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) :=
  Cofan.mk (pullback (Sigma.desc f) (Sigma.desc g)) fun p ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsUniversalColimit (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i)

pp: case refine_3
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
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) :=
  Cofan.mk (pullback (Sigma.desc f) (Sigma.desc g)) fun p ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsLimit (pullback.cone (Sigma.desc f) (Sigma.desc g))

Tactic:
· exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)

Goal state after:
case refine_3
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
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) :=
  Cofan.mk (pullback (Sigma.desc f) (Sigma.desc g)) fun p ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsLimit (pullback.cone (Sigma.desc f) (Sigma.desc g))
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case convert_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i)

Tactic:
· exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Cᵒᵖ ⥤ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
i : (unop W).shape.R
k : K
⊢ E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) ((unop W).shape.snd i) ≫ ((unop W).index (F.obj k)).snd i =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
F' : K ⥤ (J.Cover X)ᵒᵖ ⥤ D := F ⋙ J.diagramFunctor D X
e : colimit (limit (F ⋙ J.diagramFunctor D X)) ≅ limit (colimit (F ⋙ J.diagramFunctor D X).flip) :=
  colimitLimitIso (F ⋙ J.diagramFunctor D X)
t : J.diagram (limit F) X ≅ limit (F ⋙ J.diagramFunctor D X) :=
  (isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
    (limit.isLimit (F ⋙ J.diagramFunctor D X))
p : (J.plusObj (limit F)).obj (op X) ≅ colimit (limit (F ⋙ J.diagramFunctor D X)) := HasColimit.isoOfNatIso t
i j : K
f : i ⟶ j
w : (J.Cover (unop (op X)))ᵒᵖ
⊢ ((F ⋙ J.diagramFunctor D X).flip.obj w).map f ≫ (colimit.ι (F ⋙ J.diagramFunctor D X).flip w).app j =
    (J.diagramNatTrans (F.map f) (unop (op X))).app w ≫ (colimit.ι (F ⋙ J.diagramFunctor D X).flip w).app j

Tactic:
rfl

Goal state after: