mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ whiskerRight (J.toPlus P) F ≫
      ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight (J.toPlus P) F)) ≫ J.plusMap (J.plusCompIso F P).hom =
    J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F))

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ whiskerRight (J.toPlus P) F ≫
      (J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight (J.toPlus P) F) ≫ J.plusMap (J.plusCompIso F P).hom =
    J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F))
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ (η ≫ toSheafify J Q) ≫ sheafifyLift J γ hR = η ≫ γ

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ η ≫ toSheafify J Q ≫ sheafifyLift J γ hR = η ≫ γ
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
ii : W.Arrow
⊢ S.ι ii ≫ (E.π.app j).app (op ii.Y) =
    (⋯.amalgamate W (fun x ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X)) ≫ (F.obj j).obj.map ii.f.op

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
ii : W.Arrow
⊢ S.ι ii ≫ (E.π.app j).app (op ii.Y) =
    ⋯.amalgamate W (fun x ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X) ≫ (F.obj j).obj.map ii.f.op
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
ii : W.Arrow
⊢ S.ι ii ≫ (E.π.app j).app (op ii.Y) = (S.ι ii ≫ (E.π.app i).app (op ii.Y)) ≫ (F.map f).hom.app (op ii.Y)

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
ii : W.Arrow
⊢ S.ι ii ≫ (E.π.app j).app (op ii.Y) = S.ι ii ≫ (E.π.app i).app (op ii.Y) ≫ (F.map f).hom.app (op ii.Y)
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
⊢ ((isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫ E.pt.map i.f.op) ≫
      (E.π.app k).app (op i.Y) =
    S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i : W.shape.L
k : K
⊢ (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
      E.pt.map i.f.op ≫ (E.π.app k).app (op i.Y) =
    S.ι i ≫ (E.π.app k).app (op i.Y)
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj.map i.f.op = (m ≫ (W.multifork E.pt).ι i) ≫ (E.π.app k).app (op i.Y)

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ m ≫ (E.π.app k).app (op X) ≫ (F.obj k).obj.map i.f.op = (m ≫ (W.multifork E.pt).ι i) ≫ (E.π.app k).app (op i.Y)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: case e_a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x✝ : Cᵒᵖ
a : ⊤.shape.L
⊢ (F.map (⊤.toMultiequalizer P) ≫ (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤)) ≫
      Multiequalizer.ι (⊤.index (P ⋙ F)) a =
    ⊤.toMultiequalizer (P ⋙ F) ≫ Multiequalizer.ι (⊤.index (P ⋙ F)) a

Tactic:
Category.assoc,

Goal state after:
case e_a
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x✝ : Cᵒᵖ
a : ⊤.shape.L
⊢ F.map (⊤.toMultiequalizer P) ≫
      (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤) ≫ Multiequalizer.ι (⊤.index (P ⋙ F)) a =
    ⊤.toMultiequalizer (P ⋙ F) ≫ Multiequalizer.ι (⊤.index (P ⋙ F)) a
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget).sections

Tactic:
rw [← Types.hasLimit_iff_small_sections]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F ↔ HasLimit (F ⋙ forget)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ (η ≫ J.toSheafify Q) ≫ J.sheafifyLift γ hR = η ≫ γ

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ η ≫ J.toSheafify Q ≫ J.sheafifyLift γ hR = η ≫ γ
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : Cone (pair X Y)) (j : Discrete WalkingPair),
    ofHom
          {
            toFun := fun s_1 ↦
              ((ConcreteCategory.hom (BinaryFan.fst s)) s_1, (ConcreteCategory.hom (BinaryFan.snd s)) s_1),
            continuous_toFun := ⋯ } ≫
        (X.prodBinaryFan Y).π.app j =
      s.π.app j

Tactic:
by
    rintro S (_ | _) <;> {dsimp; ext; rfl}

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_4
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ m = s.inr →
        m =
          ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }

Tactic:
intro s m h₁ h₂
    ext (x | x)
    exacts [ConcreteCategory.congr_hom h₁ x, ConcreteCategory.congr_hom h₂ x]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U →
    x ∈ ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U

Tactic:
rintro ⟨y, hy, rfl⟩

Goal state after:
case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
y : ↑(pullback f g)
hy : y ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U
⊢ (ConcreteCategory.hom (pullback.snd f g)) y ∈ ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U →
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' ⇑(ConcreteCategory.hom g) '' U

Tactic:
rintro ⟨y, hy, rfl⟩

Goal state after:
case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
y : ↑(pullback f g)
hy : y ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U
⊢ (ConcreteCategory.hom (pullback.fst f g)) y ∈ ⇑(ConcreteCategory.hom f) ⁻¹' ⇑(ConcreteCategory.hom g) '' U
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsUniversalColimit c
⊢ IsUniversalColimit ((Cocone.precompose α).obj c)

Tactic:
by
  intro F' c' α' f e hα H
  apply (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) (hα.comp (.of_isIso _)))
  intro j
  simp only [NatTrans.comp_app]
  rw [← Category.comp_id f]
  exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨Category.comp_id _⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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
inst✝ : FinitaryPreExtensive C
⊢ IsIso (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).inr

Tactic:
by
      dsimp
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.refine_2.id
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 : IsVanKampenColimit (PushoutCocone.mk h i✝ ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ (span f' g').map (𝟙 i) ≫ Option.rec αW (fun val ↦ WalkingPair.rec αX αY val) i =
    Option.rec αW (fun val ↦ WalkingPair.rec αX αY val) i ≫ (span f g).map (𝟙 i)

Tactic:
simp only [Functor.map_id, Category.comp_id, Category.id_comp]

Goal state after:
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 : IsVanKampenColimit (PushoutCocone.mk h i✝ ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ 𝟙 ((span f' g').obj i) ≫ Option.rec αW (fun val ↦ WalkingPair.rec αX αY val) i =
    Option.rec αW (fun val ↦ WalkingPair.rec αX αY val) i ≫ 𝟙 ((span f g).obj i)

Tactic:
by rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case 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.IsVanKampen →
    ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
      CommSq h' αX αZ h →
        CommSq i' αY αZ i →
          ∀ [HasPullback αX f],
            IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
              ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

Tactic:
intro H' X' Y' Z' h' i' αX αY αZ sq_h sq_i _

Goal state after:
case 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
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst✝ : HasPullback αX f
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
    ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (c.inr ≫ fE) ≫ m = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
Category.assoc,

Goal state after:
case mp.refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ c.inr ≫ fE ≫ m = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: case a
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
O : Finset K := (Finset.univ.biUnion fun j ↦ Finset.univ.biUnion fun j' ↦ Finset.image kf Finset.univ) ∪ {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
k'O : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun j ↦
    Finset.univ.biUnion fun j' ↦
      Finset.univ.biUnion fun f ↦ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩ ∈ H

Tactic:
exact Finset.mem_biUnion.mpr ⟨j₁, Finset.mem_univ _,
          Finset.mem_biUnion.mpr ⟨j₂, Finset.mem_univ _,
            Finset.mem_biUnion.mpr ⟨f, Finset.mem_univ _, by
              -- This works by `simp`, but has very high variation in heartbeats.
              rw [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq,
                PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, eq_self, true_and, eq_self,
                true_and, eq_self, true_and, eq_self, true_and, Finset.mem_singleton, eq_self,
                true_or]
              trivial⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ pullback.fst αY c.inr ≫ αY ≫ i = (pullback.fst αY c.inr ≫ i') ≫ αZ

Tactic:
Category.assoc,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ pullback.fst αY c.inr ≫ αY ≫ i = pullback.fst αY c.inr ≫ i' ≫ αZ
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl =
    (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl ≫ αZ

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
· dsimp; rw [← pullback.condition_assoc, Category.assoc, hi.w]

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i