awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
G : Type u_2
inst_2 : Group G
inst_3 : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
b : ActionCategory G X
a : X
f : Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a ⟶ b
rcases :
  ∀ (b : X)
    (f :
      Quiver.Hom.{u_2, u} (V := ActionCategory G X)
        (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a)
        (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b)),
    P (a :=
        Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) ()
          (HSMul.hSMul (β := X) (↑f : ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)⁻¹
            (ActionCategory.back.{u, u_2} (M := G)
              (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
        (homOfPair
          (ActionCategory.back.{u, u_2} (M := G)
            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))
          (↑f : ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)) =
      P f
⊢ P (homOfPair b.back (↑f : ⟨PUnit.unit, a⟩.fst ⟶ b.fst)) = P f

Tactic:
rcases b with ⟨⟨⟩, b : X⟩
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
⊢ Eq (α := pullback αX f ⟶ Z) ((pullback.fst αX f ≫ h') ≫ αZ) ((pullback.snd αX f ≫ g) ≫ i)

Tactic:
simp only [Category.assoc, hh.toCommSq.w, pullback.condition_assoc, ← H.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.IsPushout.toCommSq, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
h₁ :
  IsPullback (P := pullback αX f) (pullback.fst αX f) (pullback.snd αX f) αX f ∧
    IsPullback l (pullback.snd αX f) αY g ∧ IsPushout (pullback.fst αX f) l h' i'
⊢ ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
    IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

Tactic:
use (pullback αX f), (pullback.fst αX f), l, (pullback.snd αX f)

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f) (pullback.snd αX f) αX f ∧
    IsPullback l (pullback.snd αX f) αY g ∧ IsPushout (pullback.fst αX f) l h' i'

Tactic:
⟨IsPullback.of_hasPullback αX f, ?_, ?_⟩

Premises used: And.intro, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
h₁ : IsPullback l (pullback.snd αX f) αY g
h₂ : IsPushout (pullback.fst αX f) l h' i'
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f) (pullback.snd αX f) αX f ∧
    IsPullback l (pullback.snd αX f) αY g ∧ IsPushout (pullback.fst αX f) l h' i'

Tactic:
refine ⟨IsPullback.of_hasPullback αX f, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback l (pullback.snd αX f) αY g

Tactic:
IsPullback.of_right' ?_ hi

Premises used: CategoryTheory.IsPullback.of_right'
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
h₁ : IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (g ≫ i)
⊢ IsPullback l (pullback.snd αX f) αY g

Tactic:
refine IsPullback.of_right' ?_ hi

Premises used: CategoryTheory.IsPullback.of_right'
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
h₁ : IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (f ≫ h)
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (g ≫ i)

Tactic:
rw [← H.w]

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (f ≫ h)

Tactic:
IsPullback.paste_horiz (IsPullback.of_hasPullback αX f) hh

Premises used: CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback (P := pullback αX f) (pullback.fst αX f ≫ h') (pullback.snd αX f) αZ (f ≫ h)

Tactic:
exact IsPullback.paste_horiz (IsPullback.of_hasPullback αX f) hh

Premises used: CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ pullback.fst αX f ≫ h' = l ≫ i'

Tactic:
simp only [IsPullback.lift_fst, l]

Premises used: CategoryTheory.IsPullback.lift_fst
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst_1 : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
h₁ : IsPullback l (pullback.snd αX f) αY g
⊢ IsPushout (pullback.fst αX f) l h' i'

Tactic:
refine (H' (pullback.fst αX f) l h' i' (pullback.snd αX f) αX αY αZ
      (IsPullback.of_hasPullback αX f) ?_
        hh.toCommSq hi.toCommSq ⟨by simp only [IsPullback.lift_fst, l]⟩).2 ⟨hh, hi⟩

Premises used: Iff.mpr, CategoryTheory.Limits.pullback.snd, CategoryTheory.CommSq.mk, And.intro, CategoryTheory.Limits.pullback.fst, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.toCommSq
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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' : H.IsVanKampen
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ i ∧ IsPullback i' αY αZ h

Tactic:
simpa only [IsPushout.flip_iff, IsPullback.flip_iff, and_comm] using
    H' g' f' i' h' αW αY αX αZ hg hf hi hh w.flip

Premises used: CategoryTheory.IsPullback.flip_iff, CategoryTheory.IsPushout.flip_iff, CategoryTheory.CommSq.flip, and_comm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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
mp : H.IsVanKampen → IsVanKampenColimit (PushoutCocone.mk h i ⋯)
mpr : IsVanKampenColimit (PushoutCocone.mk h i ⋯) → H.IsVanKampen
⊢ H.IsVanKampen ↔ IsVanKampenColimit (PushoutCocone.mk h i ⋯)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ IsPullback (F'.map WalkingSpan.Hom.fst) (α.app WalkingSpan.zero) (α.app WalkingSpan.left)
    ((span f g).map WalkingSpan.Hom.fst)

Tactic:
hα WalkingSpan.Hom.fst

Premises used: CategoryTheory.Limits.WalkingSpan.Hom.fst
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ IsPullback (F'.map WalkingSpan.Hom.fst) (α.app WalkingSpan.zero) (α.app WalkingSpan.left) f

Tactic:
convert! hα WalkingSpan.Hom.fst

Premises used: CategoryTheory.Limits.WalkingSpan.Hom.fst
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ IsPullback (F'.map WalkingSpan.Hom.snd) (α.app WalkingSpan.zero) (α.app WalkingSpan.right)
    ((span f g).map WalkingSpan.Hom.snd)

Tactic:
hα WalkingSpan.Hom.snd

Premises used: CategoryTheory.Limits.WalkingSpan.Hom.snd
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ IsPullback (F'.map WalkingSpan.Hom.snd) (α.app WalkingSpan.zero) (α.app WalkingSpan.right) g

Tactic:
convert! hα WalkingSpan.Hom.snd

Premises used: CategoryTheory.Limits.WalkingSpan.Hom.snd
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
mp :
  Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
mp₁ : CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
mp₂ : CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
mp₃ :
  CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)
mp₄ :
  IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)

Tactic:
refine Iff.trans ?_
        ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _)
          (α.app _) (α.app _) (α.app _) fα (by convert! hα WalkingSpan.Hom.fst)
          (by convert! hα WalkingSpan.Hom.snd) ?_ ?_ ?_).trans ?_)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.WalkingSpan.Hom.fst, Iff.trans, CategoryTheory.Limits.WalkingSpan.Hom.snd, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right

Tactic:
simp only [Cocone.w]

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right

Tactic:
have : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left =
          F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right := by
        simp only [Cocone.w]
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
mp :
  Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
rw :
  (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)

Tactic:
rw [(IsColimit.equivOfNatIsoOfIso (diagramIsoSpan F') c' (PushoutCocone.mk _ _ this)
            _).nonempty_congr]

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Limits.diagramIsoSpan, Equiv.nonempty_congr, CategoryTheory.Limits.PushoutCocone.mk
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)

Tactic:
⟨fun h => ⟨⟨this⟩, h⟩, fun h => h.2⟩

Premises used: CategoryTheory.IsPushout.isColimit', CategoryTheory.IsPushout.mk, CategoryTheory.CommSq.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)

Tactic:
exact ⟨fun h => ⟨⟨this⟩, h⟩, fun h => h.2⟩
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
refine :
  ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app j ≫ Iso.hom (Iso.refl c'.pt) =
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app j
⊢ (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this

Tactic:
refine Cocone.ext (Iso.refl c'.pt) ?_

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
none :
  (𝟙 (F'.obj Option.none) ≫ c'.ι.app Option.none) ≫ 𝟙 c'.pt = F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left
⊢ Eq (α :=
    (span (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd)).obj Option.none ⟶
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).pt)
    (((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app Option.none ≫ Iso.hom (Iso.refl c'.pt))
    ((PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app Option.none)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
some :
  (𝟙 (F'.obj (Option.some WalkingPair.left)) ≫ c'.ι.app (Option.some WalkingPair.left)) ≫ 𝟙 c'.pt =
    c'.ι.app WalkingSpan.left
⊢ Eq (α :=
    (span (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd)).obj (Option.some WalkingPair.left) ⟶
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).pt)
    (((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app (Option.some WalkingPair.left) ≫
      Iso.hom (Iso.refl c'.pt))
    ((PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app
      (Option.some WalkingPair.left))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
some :
  (𝟙 (F'.obj (Option.some WalkingPair.right)) ≫ c'.ι.app (Option.some WalkingPair.right)) ≫ 𝟙 c'.pt =
    c'.ι.app WalkingSpan.right
⊢ Eq (α :=
    (span (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd)).obj (Option.some WalkingPair.right) ⟶
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).pt)
    (((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app (Option.some WalkingPair.right) ≫
      Iso.hom (Iso.refl c'.pt))
    ((PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app
      (Option.some WalkingPair.right))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (𝟙 (F'.obj none) ≫ c'.ι.app none) ≫ 𝟙 c'.pt = F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left

Tactic:
simp only [c'.w, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.w, CategoryTheory.Category.id_comp