awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
rwa rwa₁ rwa₂ rwa₃ : Mono b
⊢ Mono (v ≫ pushout.desc a b ⋯)

Tactic:
rwa [pushout.inr_desc]

Premises used: CategoryTheory.Limits.pushout.inr_desc
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this_2 : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
this_3 : Mono f' := ⋯
sq₂₁ : IsPullback (P := pullback m₂ l₁) (fst m₂ l₁) (snd m₂ l₁) m₂ l₁ := ⋯
sq₂₂ : IsPullback (P := pullback m₂ l₂) (fst m₂ l₂) (snd m₂ l₂) m₂ l₂ := ⋯
this : Mono (v ≫ pushout.desc a b ⋯) := ⋯
i'_w :
  Eq (α := pullback m₂ l₂ ⟶ Z) ((snd m₂ l₂ ≫ snd f v) ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₁ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ snd f v ≫ v ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₂ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ f ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₃ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (snd m₂ l₂ ≫ fst f v ≫ g ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₄ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b ⋯)
    ((fst m₂ l₂ ≫ snd g v) ≫ v ≫ pushout.desc a b ⋯)
i'_w₅ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b ⋯) (fst m₂ l₂ ≫ snd g v ≫ v ≫ pushout.desc a b ⋯)
i'_w₆ i'_w₇ :
  Eq (α := pullback m₂ l₂ ⟶ Z) (fst m₂ l₂ ≫ m₂ ≫ g ≫ pushout.desc a b ⋯) (fst m₂ l₂ ≫ fst g v ≫ g ≫ pushout.desc a b ⋯)
⊢ Eq (α := pullback m₂ l₂ ⟶ B) (snd m₂ l₂ ≫ snd f v) (fst m₂ l₂ ≫ snd g v)

Tactic:
rw [← cancel_mono (v ≫ pushout.desc a b pullback.condition), Category.assoc,
          ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
          ← sq_g_v.w_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pushout.desc, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w_assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
⊢ Adhesive (Type u)

Tactic:
⟨fun {_ _ _ _ f _ _ _ _} H =>
    (IsPushout.isVanKampen_inl _ (Types.isCoprodOfMono f) _ _ _ H.flip).flip⟩

Premises used: TypeCat.ofHom, CategoryTheory.Adhesive.mk, CategoryTheory.IsPushout.flip, CategoryTheory.Limits.BinaryCofan.mk, Subtype.val, CategoryTheory.IsPushout.IsVanKampen.flip, CategoryTheory.Limits.Types.isCoprodOfMono, CategoryTheory.IsPushout.isVanKampen_inl
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : Adhesive.{v, u} C
⊢ IsRegularMonoCategory.{v, u} C

Tactic:
⟨fun f _ => ⟨⟨{
      Z := pushout f f
      left := pushout.inl _ _
      right := pushout.inr _ _
      w := pushout.condition
      isLimit := (Adhesive.isPullback_of_isPushout_of_mono_left
        (IsPushout.of_hasPushout f f)).isLimitFork }⟩⟩⟩

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.IsRegularMonoCategory.mk, CategoryTheory.Limits.pushout.condition, CategoryTheory.RegularMono.mk, Nonempty.intro, CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_left, CategoryTheory.Limits.pushout, CategoryTheory.IsPullback.isLimitFork, CategoryTheory.Limits.pushout.inl, CategoryTheory.IsRegularMono.mk, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : Adhesive.{v, u} C
⊢ Balanced.{v, u} C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
van_kampen :
  ∀ {W X Y Z : Functor.{v'', v, u'', u} D C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f]
    (H : IsPushout f g h i), H.IsVanKampen
⊢ Adhesive (Functor.{v'', v, u'', u} D C)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
van_kampen : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
⊢ H.IsVanKampen

Tactic:
rw [IsPushout.isVanKampen_iff]

Premises used: CategoryTheory.IsPushout.isVanKampen_iff
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
van_kampen :
  ∀ (x : D),
    IsVanKampenColimit (F := span f g ⋙ Functor.obj (evaluation D C) x)
      (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯)

Tactic:
apply isVanKampenColimit_of_evaluation

Premises used: CategoryTheory.isVanKampenColimit_of_evaluation
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit (F := span f g ⋙ Functor.obj (evaluation D C) x)
    (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))

Tactic:
(IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_

Premises used: CategoryTheory.Limits.diagramIsoSpan, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, Iff.mp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
van_kampen :
  IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ Functor.obj (evaluation D C) x)).inv).obj
      (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
⊢ IsVanKampenColimit (F := span f g ⋙ Functor.obj (evaluation D C) x)
    (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))

Tactic:
refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_

Premises used: CategoryTheory.Limits.diagramIsoSpan, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, Iff.mp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ Functor.obj (evaluation D C) x)).inv).obj
      (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))

Tactic:
IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm

Premises used: CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.PushoutCocone.isoMk, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
van_kampen :
  IsVanKampenColimit (F :=
    span ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.fst)
      ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.snd))
    (PushoutCocone.mk (W :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingSpan)
          (Cocone.pt (F := span f g ⋙ Functor.obj (evaluation D C) x)
            (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.right)
      ⋯)
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ Functor.obj (evaluation D C) x)).inv).obj
      (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))

Tactic:
refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm

Premises used: CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.PushoutCocone.isoMk, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit (F :=
    span ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.fst)
      ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.snd))
    (PushoutCocone.mk (W :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingSpan)
          (Cocone.pt (F := span f g ⋙ Functor.obj (evaluation D C) x)
            (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.right)
      ⋯)

Tactic:
(IsPushout.isVanKampen_iff (H.map ((evaluation _ _).obj x))).mp ?_

Premises used: Iff.mp, CategoryTheory.IsPushout.map, CategoryTheory.evaluation, CategoryTheory.Functor.obj, CategoryTheory.IsPushout.isVanKampen_iff
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
van_kampen : IsPushout.IsVanKampen (W := Functor.obj (Functor.obj (evaluation D C) x) W) ⋯
⊢ IsVanKampenColimit (F :=
    span ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.fst)
      ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.snd))
    (PushoutCocone.mk (W :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingSpan)
          (Cocone.pt (F := span f g ⋙ Functor.obj (evaluation D C) x)
            (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.right)
      ⋯)

Tactic:
refine (IsPushout.isVanKampen_iff (H.map ((evaluation _ _).obj x))).mp ?_

Premises used: Iff.mp, CategoryTheory.IsPushout.map, CategoryTheory.evaluation, CategoryTheory.Functor.obj, CategoryTheory.IsPushout.isVanKampen_iff
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsPushout.IsVanKampen (W := Functor.obj (Functor.obj (evaluation D C) x) W) ⋯

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
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
apply : ∀ {W X Y Z : C} {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} C

Tactic:
apply Adhesive.mk (hasPullback_of_mono_left := H₁) (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
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
rw : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
⊢ H.IsVanKampen

Tactic:
rw [IsPushout.isVanKampen_iff]

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
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 h i ⋯)

Tactic:
IsVanKampenColimit.of_mapCocone F ?_

Premises used: CategoryTheory.IsVanKampenColimit.of_mapCocone
-- 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 : IsVanKampenColimit (F.mapCocone (PushoutCocone.mk h i ⋯))
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯)

Tactic:
refine IsVanKampenColimit.of_mapCocone F ?_

Premises used: CategoryTheory.IsVanKampenColimit.of_mapCocone
-- 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 (F.mapCocone (PushoutCocone.mk h i ⋯))

Tactic:
(IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_

Premises used: CategoryTheory.Limits.diagramIsoSpan, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, Iff.mp, CategoryTheory.Iso.inv
-- 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 :
  IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))
⊢ IsVanKampenColimit (F.mapCocone (PushoutCocone.mk h i ⋯))

Tactic:
refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_

Premises used: CategoryTheory.Limits.diagramIsoSpan, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, Iff.mp, CategoryTheory.Iso.inv
-- 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
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))

Tactic:
IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm

Premises used: CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.PushoutCocone.isoMk, CategoryTheory.Iso.symm
-- 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 :
  IsVanKampenColimit
    (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))

Tactic:
refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm

Premises used: CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.PushoutCocone.isoMk, CategoryTheory.Iso.symm