mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.mpr.h₁
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := ⋯
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ (g'' ≫ (Iso.refl Y').hom) ≫ αY = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ αY

Tactic:
·

Goal state after:
case mpr.mpr.h₁
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := ⋯
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ (g'' ≫ (Iso.refl Y').hom) ≫ αY = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ αY
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:
classical
  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.Extensive

Goal state before:
pp: case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) ⊆
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl

pp: case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl))

Tactic:
·

Goal state after:
case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) ⊆
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl))

Tactic:
·

Goal state after:
case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl))
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) ⊆
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr

pp: case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr))

Tactic:
·

Goal state after:
case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) ⊆
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp
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
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) → IsPushout f c.inl iY fE

pp: case mpr
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
⊢ IsPushout f c.inl iY fE → Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY))

Tactic:
·

Goal state after:
case mp
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
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) → IsPushout f c.inl iY fE
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr))

Tactic:
·

Goal state after:
case a
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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_1
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
⊢ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr

pp: case mp.refine_2
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
⊢ ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
    iY ≫ m = s.inl → fE ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
·

Goal state after:
case mp.refine_1
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
⊢ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr
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.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr

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:
·

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.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
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:
·

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: 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
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
h₂ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
            (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inr)

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
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
h₂ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
⊢ IsCompl
    (Set.range
      ⇑(ConcreteCategory.hom
          (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
              (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inl))
    (Set.range
      ⇑(ConcreteCategory.hom
          (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
              (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inr))

Tactic:
·

Goal state after:
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
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
h₂ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
            (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inr)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2
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
⊢ ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
    iY ≫ m = s.inl → fE ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
·

Goal state after:
case mp.refine_2
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
⊢ ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
    iY ≫ m = s.inl → fE ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
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
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
h₂ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
⊢ IsCompl
    (Set.range
      ⇑(ConcreteCategory.hom
          (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
              (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inl))
    (Set.range
      ⇑(ConcreteCategory.hom
          (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
              (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inr))

Tactic:
·

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
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
h₂ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
⊢ IsCompl
    (Set.range
      ⇑(ConcreteCategory.hom
          (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
              (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inl))
    (Set.range
      ⇑(ConcreteCategory.hom
          (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
              (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inr))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2.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
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

pp: case mp.refine_2.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
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
·

Goal state after:
case mp.refine_2.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
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl