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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (v ≫ v')

Tactic:
← Sieve.ofArrows.fac hv',

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (v ≫ Sieve.ofArrows.h hv' ≫ f (Sieve.ofArrows.i hv'))
Module: Mathlib.CategoryTheory.Sites.Plus

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 : Cᵒᵖ ⥤ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
⊢ γ = J.plusLift (J.toPlus P ≫ γ) hQ

Tactic:
apply plusLift_unique

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 : Cᵒᵖ ⥤ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
⊢ J.toPlus P ≫ γ = J.toPlus P ≫ γ
Module: Mathlib.CategoryTheory.Sites.Plus

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 : Cᵒᵖ ⥤ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
⊢ η = J.plusLift (J.toPlus P ≫ γ) hQ

Tactic:
apply plusLift_unique

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 : Cᵒᵖ ⥤ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
⊢ J.toPlus P ≫ η = J.toPlus P ≫ γ
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
e : parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
  parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext (PreservesProduct.iso s fun f ↦ P.obj (op f.fst))
    (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ⋯ ⋯
⊢ IsLimit (s.mapCone (Fork.ofι (forkMap R P) ⋯)) ≃ IsLimit (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)

Tactic:
refine Equiv.trans (isLimitMapConeForkEquiv _ _) ?_

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
e : parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
  parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext (PreservesProduct.iso s fun f ↦ P.obj (op f.fst))
    (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ⋯ ⋯
⊢ IsLimit (Fork.ofι (s.map (forkMap R P)) ⋯) ≃ IsLimit (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)
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
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom (P.map II.r.g₁.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst) =
    (ConcreteCategory.hom (P.map II.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd)

Tactic:
apply inj_of_sep P hsep

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.toPlus P).app (op II.r.Z)))
      ((ConcreteCategory.hom (P.map II.r.g₁.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst)) =
    (ConcreteCategory.hom ((J.toPlus P).app (op II.r.Z)))
      ((ConcreteCategory.hom (P.map II.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd))
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ({ hom := (isoSheafify J ⋯).hom } ≫ { hom := (isoSheafify J ⋯).inv }).hom = (𝟙 P).hom

Tactic:
apply (isoSheafify J P.2).hom_inv_id

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W ≫ colimMap (J.diagramNatTrans η (unop X))) ≫ (J.plusCompIso F Q).hom.app X =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) ((J.diagram (P ⋙ F) (unop X)).obj W)
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      colimit.ι (J.diagram (Q ⋙ F) (unop X)) W

Tactic:
dsimp [colimMap, IsColimit.map]

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (colimit.ι (J.diagram P (unop X)) W ≫
          colimit.desc (J.diagram P (unop X))
            ((Cocone.precompose (J.diagramNatTrans η (unop X))).obj (colimit.cocone (J.diagram Q (unop X))))) ≫
      (J.plusCompIso F Q).hom.app X =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
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 : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ γ = J.sheafifyLift η hQ

Tactic:
apply plusLift_unique

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 : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ J.toPlus (J.plusObj P) ≫ γ = J.plusLift η hQ
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 : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ J.toPlus (J.plusObj P) ≫ γ = J.plusLift η hQ

Tactic:
apply plusLift_unique

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 : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ = η
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case convert_1
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ (const K).map f

Tactic:
convert! congr_arg (whiskerLeft e.inverse) e'
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case right
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
⊢ Mono (Cofan.inj c WalkingPair.right)

Tactic:
· exact inferInstanceAs <| Mono c.inr

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_obj
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := ⋯
Y : C := ⋯
⊢ ∀ (X_1 : Discrete WalkingPair), F.obj X_1 = (pair X Y).obj X_1

pp: case h_map
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := ⋯
Y : C := ⋯
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), F.map f ≍ (pair X Y).map f

Tactic:
· rintro ⟨⟨⟩⟩ <;> rfl

Goal state after:
case h_map
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := ⋯
Y : C := ⋯
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), F.map f ≍ (pair X Y).map f
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✝¹ : HasBinaryCoproducts C
inst✝ : HasPullbacksOfInclusions C
X Y Z : C
f : Z ⟶ X ⨿ Y
⊢ HasPullback f coprod.inr

Tactic:
have : IsPullback (𝟙 _) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom :=
    IsPullback.of_horiz_isIso ⟨by simp⟩
  have := (IsPullback.of_hasPullback (f ≫ (coprod.braiding X Y).hom) coprod.inl).paste_horiz this
  simp only [coprod.braiding_hom, Category.comp_id, colimit.ι_desc,
    BinaryCofan.ι_app_left, BinaryCofan.mk_inl] at this
  exact ⟨⟨⟨_, this.isLimit⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
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
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ { l //
    l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).snd = s.snd → m = l }

Tactic:
have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · simp

Goal state after:
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
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
this : ∀ (x : (fun X ↦ X) s.pt), ∃! y, (ConcreteCategory.hom s.fst) x = Sum.inr y
⊢ { l //
    l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝)) αY✝ ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case 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' :
  ∀ ⦃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'
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),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)

Tactic:
αW

Goal state after:
case 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' :
  ∀ ⦃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'
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),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_1.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
⊢ c.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr

pp: case mp.refine_1.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
⊢ c.inr ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
· rw [← H.w_assoc]; erw [h.fac _ ⟨WalkingPair.right⟩]; exact s.condition

Goal state after:
case mp.refine_1.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
⊢ c.inr ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_obj
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ ∀ (X_1 : Discrete WalkingPair), (pair X Y ⋙ Gr).obj X_1 = (pair (Gr.obj X) (Gr.obj Y)).obj X_1

pp: case h_map
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), (pair X Y ⋙ Gr).map f ≍ (pair (Gr.obj X) (Gr.obj Y)).map f

Tactic:
· rintro ⟨⟨⟩⟩ <;> rfl

Goal state after:
case h_map
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), (pair X Y ⋙ Gr).map f ≍ (pair (Gr.obj X) (Gr.obj Y)).map f
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
m : E.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt
hm :
  ∀ (j : K),
    m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j
a : (unop W).shape.L
j : K
⊢ m ≫ Multiequalizer.ι ((unop W).index (limit F)) a ≫ (limit.π F j).app (op a.Y) =
    liftToDiagramLimitObjAux F E a ≫ (limit.π F j).app (op a.Y)

Tactic:
liftToDiagramLimitObjAux_fac,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
m : E.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt
hm :
  ∀ (j : K),
    m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j
a : (unop W).shape.L
j : K
⊢ m ≫ Multiequalizer.ι ((unop W).index (limit F)) a ≫ (limit.π F j).app (op a.Y) =
    E.π.app j ≫ Multiequalizer.ι ((unop W).index (F.obj j)) a