awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
refine_1 :
  ∀ (F G : Functor.{v, v', u, u'} C D)
    (h :
      Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
        ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
        ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G))
    (X : C), F.obj X = G.obj X
refine_2 :
  ∀ (F G : Functor.{v, v', u, u'} C D)
    (h :
      Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
        ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
        ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G))
    (X Y : C) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
⊢ Small.{w, max (max (max u' u) v') v} (Functor.{v, v', u, u'} C D)

Tactic:
refine small_of_injective (f := fun F (f : Arrow C) ↦ Arrow.mk (F.map f.hom))
    (fun F G h ↦ Functor.ext (fun X ↦ ?_) (fun X Y f ↦ ?_))

Premises used: CategoryTheory.Functor.ext, small_of_injective
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X : C
⊢ F.obj X = G.obj X

Tactic:
congr_arg Comma.left (congr_fun h (Arrow.mk (𝟙 X)))

Premises used: CategoryTheory.Comma.left, CategoryTheory.CategoryStruct.id, congr_arg, congr_fun, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X : C
⊢ F.obj X = G.obj X

Tactic:
exact congr_arg Comma.left (congr_fun h (Arrow.mk (𝟙 X)))

Premises used: CategoryTheory.Comma.left, CategoryTheory.CategoryStruct.id, congr_arg, congr_fun, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X Y : C
f : X ⟶ Y
⊢ Arrow.mk (F.map f) = Arrow.mk (G.map f)

Tactic:
have : Arrow.mk (F.map f) = Arrow.mk (G.map f) := congr_fun h (Arrow.mk f)
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X Y : C
f : X ⟶ Y
this : Arrow.mk (F.map f) = Arrow.mk (G.map f)
⊢ ∃ (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y), F.map f = eqToHom hX ≫ G.map f ≫ eqToHom ⋯

Tactic:
rw [Arrow.mk_eq_mk_iff] at this

Premises used: CategoryTheory.Arrow.mk_eq_mk_iff
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X Y : C
f : X ⟶ Y
this : ∃ (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y), F.map f = eqToHom hX ≫ G.map f ≫ eqToHom ⋯
refine_2 refine_2₁ refine_2₂ :
  ∀ (w : F.obj X = G.obj X) (w_1 : F.obj Y = G.obj Y),
    F.map f = eqToHom w ≫ G.map f ≫ eqToHom ⋯ → F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.EssentiallySmall
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : LocallySmall.{w, v', u'} A
C : Type w
inst_3 : SmallCategory C
P Q : Functor.{w, v', w, u'} C A
f g : P ⟶ Q
h : f.app = g.app
⊢ f = g

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
h_obj : ∀ (X_1 : Discrete WalkingPair), F.obj X_1 = Functor.obj.{0, v, 0, u} (pair X Y) X_1
h_map :
  ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1),
    HEq (F.map f) (β := Functor.obj.{0, v, 0, u} (pair X Y) X_1 ⟶ Functor.obj.{0, v, 0, u} (pair X Y) Y_1)
      (Functor.map (pair X Y) f)
⊢ F = pair X Y

Tactic:
apply Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (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 : Discrete WalkingPair } =
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (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 : Discrete WalkingPair } =
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ HEq
    (F.map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := WalkingPair.left : Discrete WalkingPair }.as =
                { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair }.as) } :
        ULift.{0, 0}
          (PLift
            ({ as := WalkingPair.left : Discrete WalkingPair }.as =
              { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair }.as)) })
    (β :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y)
        { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair })
    (Functor.map (pair X Y) { down := { down := ⋯ } })

Tactic:
simp [X, Y]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ HEq
    (F.map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := WalkingPair.right : Discrete WalkingPair }.as =
                { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair }.as) } :
        ULift.{0, 0}
          (PLift
            ({ as := WalkingPair.right : Discrete WalkingPair }.as =
              { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair }.as)) })
    (β :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y)
        { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair })
    (Functor.map (pair X Y) { down := { down := ⋯ } })

Tactic:
simp [X, Y]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ F = pair X Y

Tactic:
have : F = pair X Y := by
    apply Functor.hext
    · rintro ⟨⟨⟩⟩ <;> rfl
    · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X, Y]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (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
clear_value : ∀ (X Y : C) (this : F = pair X Y), IsVanKampenColimit c
⊢ IsVanKampenColimit c

Tactic:
clear_value X Y
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X Y : C
this : F = pair X Y
subst : ∀ (c : Cocone.{0, v, 0, u} (pair X Y)) (hc : IsColimit c), IsVanKampenColimit c
⊢ IsVanKampenColimit c

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
X Y : C
c : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
FinitaryExtensive.van_kampen' c hc

Premises used: CategoryTheory.FinitaryExtensive.van_kampen'
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
X Y : C
c : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
exact FinitaryExtensive.van_kampen' c hc

Premises used: CategoryTheory.FinitaryExtensive.van_kampen'
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacks.{v, u} C
⊢ HasPullbacksOfInclusions.{v, u} C

Tactic:
⟨⟩

Premises used: CategoryTheory.HasPullbacksOfInclusions.mk
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ HasPullback f coprod.inl

Tactic:
hasPullback_symmetry _ _

Premises used: CategoryTheory.Limits.hasPullback_symmetry
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ 𝟙 Z ≫ f =
    CategoryStruct.comp (Y := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)

Tactic:
have : IsPullback (𝟙 _) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom :=
    IsPullback.of_horiz_isIso ⟨by simp⟩
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
this :
  IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
⊢ IsPullback (P :=
    pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (coprod.inl : Y ⟶ coprod.{v, u} Y X))
    (pullback.fst (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl ≫ 𝟙 Z :
      pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
          (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
        Z)
    (pullback.snd (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl :
      pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
          (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
        Y)
    f
    (CategoryStruct.comp (Y := coprod.{v, u} Y X) (coprod.inl : Y ⟶ coprod.{v, u} Y X)
      (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y))

Tactic:
have := (IsPullback.of_hasPullback (f ≫ (coprod.braiding X Y).hom) coprod.inl).paste_horiz this
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
this_1 :
  IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
this :
  IsPullback (P :=
    pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (coprod.inl : Y ⟶ coprod.{v, u} Y X))
    (pullback.fst (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl ≫ 𝟙 Z :
      pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
          (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
        Z)
    (pullback.snd (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl :
      pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
          (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
        Y)
    f
    (CategoryStruct.comp (Y := coprod.{v, u} Y X) (coprod.inl : Y ⟶ coprod.{v, u} Y X)
      (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y))
⊢ IsPullback (P := pullback (Z := coprod.{v, u} Y X) (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
    (pullback.fst (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
    (pullback.snd (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl) f coprod.inr

Tactic:
simp only [coprod.braiding_hom, Category.comp_id, colimit.ι_desc, BinaryCofan.mk_pt,
    BinaryCofan.ι_app_left, BinaryCofan.mk_inl] at this

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Category.comp_id, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.coprod.braiding_hom, CategoryTheory.Limits.BinaryCofan.ι_app_left
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
this_1 :
  IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
this :
  IsPullback (P := pullback (Z := coprod.{v, u} Y X) (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
    (pullback.fst (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
    (pullback.snd (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl) f coprod.inr
⊢ HasPullback f coprod.inr

Tactic:
⟨⟨⟨_, this.isLimit⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
this_1 :
  IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
this :
  IsPullback (P := pullback (Z := coprod.{v, u} Y X) (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
    (pullback.fst (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
    (pullback.snd (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl) f coprod.inr
⊢ HasPullback f coprod.inr

Tactic:
exact ⟨⟨⟨_, this.isLimit⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ HasPullback coprod.inr f

Tactic:
hasPullback_symmetry _ _

Premises used: CategoryTheory.Limits.hasPullback_symmetry
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X Y : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesLimitsOfShape WalkingCospan F
⊢ PreservesPullbacksOfInclusions F

Tactic:
⟨⟩

Premises used: CategoryTheory.PreservesPullbacksOfInclusions.mk
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ PreservesLimit (cospan f coprod.inl) F

Tactic:
preservesPullback_symmetry _ _ _

Premises used: CategoryTheory.Limits.preservesPullback_symmetry
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
h :
  cospan (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (coprod.inl : Y ⟶ coprod.{v, u} Y X) ≅
    cospan f coprod.inr
⊢ PreservesLimit (cospan f coprod.inr) F

Tactic:
apply preservesLimit_of_iso_diagram (K₁ := cospan (f ≫ (coprod.braiding X Y).hom) coprod.inl)

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
h :
  Iso.hom (Iso.refl Z) ≫ f =
    CategoryStruct.comp (Y := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (Iso.hom (Iso.symm (coprod.braiding X Y)) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
h₁ :
  Eq.{v + 1} (α := Y ⟶ coprod.{v, u} X Y) (Iso.hom (Iso.refl Y) ≫ coprod.inr : Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} Y X) (coprod.inl : Y ⟶ coprod.{v, u} Y X)
        (Iso.hom (Iso.symm (coprod.braiding X Y)) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y) :
      Y ⟶ coprod.{v, u} X Y)
⊢ cospan (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (coprod.inl : Y ⟶ coprod.{v, u} Y X) ≅
    cospan f coprod.inr

Tactic:
apply cospanExt (Iso.refl _) (Iso.refl _) (coprod.braiding X Y).symm

Premises used: CategoryTheory.Limits.coprod.braiding, CategoryTheory.Iso.refl, CategoryTheory.Limits.cospanExt, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ Iso.hom (Iso.refl Z) ≫ f =
    CategoryStruct.comp (Y := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (Iso.hom (Iso.symm (coprod.braiding X Y)) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ Eq.{v + 1} (α := Y ⟶ coprod.{v, u} X Y) (Iso.hom (Iso.refl Y) ≫ coprod.inr : Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} Y X) (coprod.inl : Y ⟶ coprod.{v, u} Y X)
        (Iso.hom (Iso.symm (coprod.braiding X Y)) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y) :
      Y ⟶ coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ PreservesLimit (cospan coprod.inr f) F

Tactic:
preservesPullback_symmetry _ _ _

Premises used: CategoryTheory.Limits.preservesPullback_symmetry
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
inst_3 : FinitaryExtensive.{v, u} C
⊢ FinitaryPreExtensive.{v, u} C

Tactic:
⟨fun c hc ↦ (FinitaryExtensive.van_kampen' c hc).isUniversal⟩

Premises used: CategoryTheory.FinitaryExtensive.van_kampen', CategoryTheory.IsVanKampenColimit.isUniversal, CategoryTheory.FinitaryPreExtensive.mk
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : FinitaryExtensive.{v, u} C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
⊢ Mono c.inr

Tactic:
BinaryCofan.mono_inr_of_isVanKampen (FinitaryExtensive.vanKampen c hc)

Premises used: CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen