awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)

Tactic:
(IsPushout.isVanKampen_iff (H.map F)).mp ?_

Premises used: Iff.mp, CategoryTheory.IsPushout.map, CategoryTheory.IsPushout.isVanKampen_iff
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
refine : ⋯.IsVanKampen
⊢ IsVanKampenColimit
    (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)

Tactic:
refine (IsPushout.isVanKampen_iff (H.map F)).mp ?_

Premises used: Iff.mp, CategoryTheory.IsPushout.map, CategoryTheory.IsPushout.isVanKampen_iff
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ ⋯.IsVanKampen

Tactic:
apply Adhesive.van_kampen

Premises used: CategoryTheory.Adhesive.van_kampen
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape WalkingSpan F
inst_7 : F.ReflectsIsomorphisms
⊢ ReflectsLimitsOfShape WalkingCospan F

Tactic:
haveI : ReflectsLimitsOfShape WalkingCospan F :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape WalkingSpan F
inst_7 : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ ReflectsColimitsOfShape WalkingSpan F

Tactic:
haveI : ReflectsColimitsOfShape WalkingSpan F :=
    reflectsColimitsOfShape_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape WalkingSpan F
inst_7 : F.ReflectsIsomorphisms
this_1 : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape WalkingSpan F
⊢ Adhesive.{v, u} C

Tactic:
adhesive_of_preserves_and_reflects F

Premises used: CategoryTheory.adhesive_of_preserves_and_reflects
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape WalkingSpan F
inst_7 : F.ReflectsIsomorphisms
this_1 : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape WalkingSpan F
⊢ Adhesive.{v, u} C

Tactic:
exact adhesive_of_preserves_and_reflects F

Premises used: CategoryTheory.adhesive_of_preserves_and_reflects
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
⊢ PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl

Tactic:
have := adj.leftAdjoint_preservesColimits
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
⊢ PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr

Tactic:
have := adj.rightAdjoint_preservesLimits
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
apply : ∀ {W X Y Z : D} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen
⊢ Adhesive.{v'', u''} D

Tactic:
apply Adhesive.mk (hasPushout_of_mono_left := H₂)

Premises used: CategoryTheory.Adhesive.mk
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
_ : ∀ [Mono f] (H : IsPushout f g h i), H.IsVanKampen
⊢ ∀ [Mono f] (H : IsPushout f g h i), H.IsVanKampen

Tactic:
_
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
⊢ IsPushout.IsVanKampen (Z := pushout (Gr.map f) (Gr.map g)) ⋯

Tactic:
have := Adhesive.van_kampen (IsPushout.of_hasPushout (Gr.map f) (Gr.map g))
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this : IsPushout.IsVanKampen (Z := pushout (Gr.map f) (Gr.map g)) ⋯
rw :
  ∀
    (this :
      IsVanKampenColimit
        (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
          (pushout.inr (Gr.map f) (Gr.map g)) ⋯)),
    IsVanKampenColimit (PushoutCocone.mk h i ⋯)
⊢ H.IsVanKampen

Tactic:
rw [IsPushout.isVanKampen_iff] at this ⊢

Premises used: CategoryTheory.IsPushout.isVanKampen_iff
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
refine :
  IsVanKampenColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯)

Tactic:
refine (IsVanKampenColimit.precompose_isIso_iff
    (Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp ?_

Premises used: CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, CategoryTheory.Adjunction.counit, CategoryTheory.Iso.trans, Iff.mp, CategoryTheory.Iso.hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsVanKampenColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Tactic:
((this.precompose_isIso (spanCompIso _ _ _).hom).map_reflective adj).of_iso
    (IsColimit.uniqueUpToIso ?_ ?_)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.spanCompIso, CategoryTheory.IsVanKampenColimit.precompose_isIso, CategoryTheory.IsVanKampenColimit.map_reflective, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Iso.hom, CategoryTheory.Limits.span
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
refine_1 :
  IsColimit
    (Gl.mapCocone
      ((Cocone.precompose (spanCompIso Gr f g).hom).obj
        (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
          (pushout.inr (Gr.map f) (Gr.map g)) ⋯)))
refine_2 :
  IsColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))
⊢ IsVanKampenColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Tactic:
refine ((this.precompose_isIso (spanCompIso _ _ _).hom).map_reflective adj).of_iso
    (IsColimit.uniqueUpToIso ?_ ?_)

Premises used: CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.spanCompIso, CategoryTheory.IsVanKampenColimit.precompose_isIso, CategoryTheory.IsVanKampenColimit.map_reflective, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    (Gl.mapCocone
      ((Cocone.precompose (spanCompIso Gr f g).hom).obj
        (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
          (pushout.inr (Gr.map f) (Gr.map g)) ⋯)))

Tactic:
exact isColimitOfPreserves Gl ((IsColimit.precomposeHomEquiv _ _).symm <| pushoutIsPushout _ _)

Premises used: CategoryTheory.Limits.pushoutIsPushout, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Tactic:
exact (IsColimit.precomposeHomEquiv _ _).symm H.isColimit

Premises used: CategoryTheory.IsPushout.isColimit, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Adhesive.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Adhesive.{v_1, u_1} C
inst_2 : HasPullbacks.{v_1, u_1} C
inst_3 : HasPushouts.{v_1, u_1} C
B : C
⊢ Adhesive (Over.{v_1, u_1} B)

Tactic:
adhesive_of_preserves_and_reflects_isomorphism (Over.forget B)

Premises used: CategoryTheory.Over.forget, CategoryTheory.adhesive_of_preserves_and_reflects_isomorphism
-- Module: Mathlib.CategoryTheory.Adhesive.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
a b : Subobject.{v, u} X
s : BinaryCofan a b
h :
  Eq (α := Limits.pullback a.arrow b.arrow ⟶ X)
    ((pullback.fst a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.left })) ≫
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.left : Discrete WalkingPair }).arrow)
    ((pullback.snd a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.right })) ≫
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.left : Discrete WalkingPair }).arrow)
⊢ Eq (α :=
    Limits.pullback a.arrow b.arrow ⟶
      Functor.obj underlying
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.left : Discrete WalkingPair }))
    (pullback.fst a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.left }))
    (pullback.snd a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.right }))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adhesive.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
a b : Subobject.{v, u} X
s : BinaryCofan a b
⊢ Eq (α := Limits.pullback a.arrow b.arrow ⟶ X)
    ((pullback.fst a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.left })) ≫
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.left : Discrete WalkingPair }).arrow)
    ((pullback.snd a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.right })) ≫
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.left : Discrete WalkingPair }).arrow)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Adhesive.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
a b : Subobject.{v, u} X
s : BinaryCofan a b
⊢ CategoryStruct.comp (Y :=
      Subobject.mk (A :=
        pushout (X := Limits.pullback a.arrow b.arrow) (pullback.fst a.arrow b.arrow) (pullback.snd a.arrow b.arrow))
        (pushout.desc a.arrow b.arrow ⋯))
      (LE.le.hom ⋯)
      ((fun (s : BinaryCofan a b) ↦
          (LE.le.hom ⋯ :
            Subobject.mk (A :=
                pushout (X := Limits.pullback a.arrow b.arrow) (pullback.fst a.arrow b.arrow)
                  (pullback.snd a.arrow b.arrow))
                (pushout.desc a.arrow b.arrow ⋯) ⟶
              Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                { as := WalkingPair.left : Discrete WalkingPair }))
        s) =
    s.inl

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adhesive.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
a b : Subobject.{v, u} X
s : BinaryCofan a b
⊢ CategoryStruct.comp (Y :=
      Subobject.mk (A :=
        pushout (X := Limits.pullback a.arrow b.arrow) (pullback.fst a.arrow b.arrow) (pullback.snd a.arrow b.arrow))
        (pushout.desc a.arrow b.arrow ⋯))
      (LE.le.hom ⋯)
      ((fun (s : BinaryCofan a b) ↦
          (LE.le.hom ⋯ :
            Subobject.mk (A :=
                pushout (X := Limits.pullback a.arrow b.arrow) (pullback.fst a.arrow b.arrow)
                  (pullback.snd a.arrow b.arrow))
                (pushout.desc a.arrow b.arrow ⋯) ⟶
              Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                { as := WalkingPair.left : Discrete WalkingPair }))
        s) =
    s.inr

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adhesive.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
a b : Subobject.{v, u} X
s : BinaryCofan a b
m :
  Subobject.mk (A :=
      pushout (X := Limits.pullback a.arrow b.arrow) (pullback.fst a.arrow b.arrow) (pullback.snd a.arrow b.arrow))
      (pushout.desc a.arrow b.arrow ⋯) ⟶
    s.pt
h : LE.le.hom ⋯ ≫ m = s.inl
h_1 : LE.le.hom ⋯ ≫ m = s.inr
⊢ m =
    (fun (s : BinaryCofan a b) ↦
        (LE.le.hom ⋯ :
          Subobject.mk (A :=
              pushout (X := Limits.pullback a.arrow b.arrow) (pullback.fst a.arrow b.arrow)
                (pullback.snd a.arrow b.arrow))
              (pushout.desc a.arrow b.arrow ⋯) ⟶
            Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
              { as := WalkingPair.left : Discrete WalkingPair }))
      s

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adhesive.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
F : Discrete WalkingPair ⥤ Subobject.{v, u} X
⊢ HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))

Tactic:
have : HasColimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isColimitBinaryCofan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Adhesive.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
F : Discrete WalkingPair ⥤ Subobject.{v, u} X
this : HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
⊢ HasColimit F

Tactic:
apply hasColimit_of_iso (diagramIsoPair F)

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.diagramIsoPair
-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X Y : D
f g : X ⟶ Y
⊢ Eq.{v₂ + 1} (α := F.obj (G.obj X) ⟶ Y)
    (((Equiv.symm (adj.homEquiv (G.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (G.obj X ⟶ G.obj Y) (F.obj (G.obj X) ⟶ Y)) :
          (a : G.obj X ⟶ G.obj Y) → F.obj (G.obj X) ⟶ Y)
        (G.map (f + g)) :
      F.obj (G.obj X) ⟶ Y)
    (((Equiv.symm (adj.homEquiv (G.obj X) Y) : Equiv.{v₁ + 1, v₂ + 1} (G.obj X ⟶ G.obj Y) (F.obj (G.obj X) ⟶ Y)) :
          (a : G.obj X ⟶ G.obj Y) → F.obj (G.obj X) ⟶ Y)
        (G.map f + G.map g) :
      F.obj (G.obj X) ⟶ Y)

Tactic:
simp [homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_counit