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

Goal state before:
pp: case mp.refine_1
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map 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)

pp: 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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this

Tactic:
·

Goal state after:
case mp.refine_1
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map 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)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: 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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this

Tactic:
·

Goal state after:
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

pp: case mpr
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')

Tactic:
·

Goal state after:
case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mpr
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')

Tactic:
·

Goal state after:
case mpr
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h

pp: case mp.refine_3
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

pp: case mp.refine_4
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)

pp: case mp.refine_5
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ 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)

Tactic:
·

Goal state after:
case mp.refine_2
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
⊢ ∀ {X' Y' : Type u} (αX : X' ⟶ PUnit.{u + 1}) (αY : Y' ⟶ PUnit.{u + 1})
    (f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

pp: case h₂
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
⊢ {Z : Type u} →
    (f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.fst
            (Types.pullbackLimitCone f
                (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))).cone)
          (PullbackCone.fst
            (Types.pullbackLimitCone f
                (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))).cone))

Tactic:
·

Goal state after:
case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
⊢ ∀ {X' Y' : Type u} (αX : X' ⟶ PUnit.{u + 1}) (αY : Y' ⟶ PUnit.{u + 1})
    (f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_3
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

pp: case mp.refine_4
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)

pp: case mp.refine_5
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ 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)

Tactic:
·

Goal state after:
case mp.refine_3
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_4
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)

pp: case mp.refine_5
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ 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)

Tactic:
·

Goal state after:
case mp.refine_4
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_5.mp
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ 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)

pp: case mp.refine_5.mpr
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ (∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)) →
    IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

Tactic:
·

Goal state after:
case mp.refine_5.mp
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ 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)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁.left
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ f
    (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

pp: case h₁.right
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
⊢ IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ f
    (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
·

Goal state after:
case h₁.left
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ f
    (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_5.mp.none
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app none) (α.app none) fα ((PushoutCocone.mk h i ⋯).ι.app none)

pp: case mp.refine_5.mp.some.left
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app (some WalkingPair.left)) (α.app (some WalkingPair.left)) fα
    ((PushoutCocone.mk h i ⋯).ι.app (some WalkingPair.left))

pp: case mp.refine_5.mp.some.right
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app (some WalkingPair.right)) (α.app (some WalkingPair.right)) fα
    ((PushoutCocone.mk h i ⋯).ι.app (some WalkingPair.right))

Tactic:
·

Goal state after:
case mp.refine_5.mp.none
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
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app none) (α.app none) fα ((PushoutCocone.mk h i ⋯).ι.app none)