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

Goal state before:
pp: case e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
⊢ Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagram P (unop Z)).map e.inv.op =
    Multiequalizer.lift (((unop S).pullback f.unop).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
        ((J.diagram P (unop Y)).obj (op ((unop S).pullback f.unop)))
        (fun I ↦ Multiequalizer.ι (((unop S).pullback f.unop).index P) (Cover.Arrow.base I)) ⋯

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)

Goal state after:
case e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
I : (unop (op (((unop S).pullback f.unop).pullback g.unop))).shape.L
⊢ (Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagram P (unop Z)).map e.inv.op) ≫
      Multiequalizer.ι ((unop (op (((unop S).pullback f.unop).pullback g.unop))).index P) I =
    (Multiequalizer.lift (((unop S).pullback f.unop).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          ((J.diagram P (unop Y)).obj (op ((unop S).pullback f.unop)))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback f.unop).index P) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop (op (((unop S).pullback f.unop).pullback g.unop))).index P) I
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
⊢ (P.map f ≫ Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯) ≫
      (J.diagram P (unop Y)).map e.op =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop X))) (fun I ↦ P.map I.f.op) ⋯ ≫
      Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P) ((J.diagram P (unop X)).obj (op ⊤))
        (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.base I)) ⋯

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)

Goal state after:
case e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
I : (unop (op ((J.pullback f.unop).obj ⊤))).shape.L
⊢ ((P.map f ≫ Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯) ≫
        (J.diagram P (unop Y)).map e.op) ≫
      Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I =
    (Multiequalizer.lift (⊤.index P) (P.obj (op (unop X))) (fun I ↦ P.map I.f.op) ⋯ ≫
        Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P) ((J.diagram P (unop X)).obj (op ⊤))
          (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ (J.diagramNatTrans { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
          (unop X)).app
      S =
    (colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
      (J.diagram (J.plusObj P) (unop X)).map e.op

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)

Goal state after:
case e_a
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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
⊢ (J.diagramNatTrans { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
            (unop X)).app
        S ≫
      Multiequalizer.ι ((unop S).index (J.plusObj P)) I =
    ((colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
        (J.diagram (J.plusObj P) (unop X)).map e.op) ≫
      Multiequalizer.ι ((unop S).index (J.plusObj P)) I
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
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J (P ⋙ s)
⊢ IsSheaf J P

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢
  exact fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfReflects s t

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      (ConcreteCategory.hom (P.map f.op)) t₁ = (FamilyOfElements.singletonEquiv P f).symm b f ⋯ →
        (ConcreteCategory.hom (P.map f.op)) t₂ = (FamilyOfElements.singletonEquiv P f).symm b f ⋯ → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))

Tactic:
FamilyOfElements.singletonEquiv_symm_apply_self,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      (ConcreteCategory.hom (P.map f.op)) t₁ = b → (ConcreteCategory.hom (P.map f.op)) t₂ = b → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))
Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
obtain ⟨h⟩ := hP X S

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case left
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)
inst✝ : (forget D).ReflectsIsomorphisms
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
x y : (forget D).obj ((J.plusObj P).obj (op X))
I : S.Arrow
h :
  (Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) x) =
    (Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) y)
⊢ (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x = (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y

Tactic:
apply_fun fun e => e I at h

Goal state after:
case left
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)
inst✝ : (forget D).ReflectsIsomorphisms
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
x y : (forget D).obj ((J.plusObj P).obj (op X))
I : S.Arrow
h :
  ↑((Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) x)) I =
    ↑((Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) y)) I
⊢ (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x = (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
⊢ ∀ (s : Cone (Discrete.functor α)) (m : s.pt ⟶ (piFan α).pt),
    (∀ (j : Discrete ι), m ≫ (piFan α).π.app j = s.π.app j) →
      m = ofHom { toFun := fun s_1 i ↦ (ConcreteCategory.hom (s.π.app { as := i })) s_1, continuous_toFun := ⋯ }

Tactic:
by
    intro S m h
    ext x
    funext i
    simp [ContinuousMap.coe_mk, ← h ⟨i⟩]

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

Goal state before:
pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ ↑((ConcreteCategory.hom m) x) =
    ↑((ConcreteCategory.hom
          (ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }))
        x)

Tactic:
apply Prod.ext

Goal state after:
case property.refine_3.fst
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).1 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).1

case property.refine_3.snd
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).2 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).2
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩

Tactic:
by
    apply Continuous.subtype_mk
    refine continuous_subtype_val.prodMk <| hg.isInducing.continuous_iff.mpr ?_
    convert! hf.comp continuous_subtype_val
    ext x
    exact Exists.choose_spec x.2

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

Goal state before:
pp: case mp
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ (∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)) →
    IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

pp: case mpr
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)

Tactic:
· intro h
    exact h .one

Goal state after:
case mpr
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).pt ⟶ T✝
h₁ : (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl ≫ m = f₁
h₂ : (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inr ≫ m = f₂
x : B
⊢ (ConcreteCategory.hom m).toFun (Sum.inr x) =
    (ConcreteCategory.hom
          (↾fun x ↦ Sum.casesOn x (fun x ↦ (ConcreteCategory.hom f₁) x) fun x ↦ (ConcreteCategory.hom f₂) x)).toFun
      (Sum.inr x)

Tactic:
exact ConcreteCategory.congr_hom h₂ x

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan X
hc : IsColimit c
inst✝ : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt
d : Cofan X
hd : IsColimit d
i : ι
⊢ Mono (d.inj i)

Tactic:
by
    rw [show d.inj i = c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom by simp]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
hl : IsPullback c.inl (HT.from X) d c₀.inl
hr : IsPullback c.inr (HT.from Y) d c₀.inr
⊢ IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
hl.paste_vert_iff hX.symm,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
hl : IsPullback c.inl (HT.from X) d c₀.inl
hr : IsPullback c.inr (HT.from Y) d c₀.inr
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case h'_w.h'_w
J : Type v'
inst✝⁴ : Category.{u', v'} J
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✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := ⋯
v : B ⟶ pushout (fst a b) (snd a b) := ⋯
this✝¹ : Mono u := ⋯
this✝ : Mono v := ⋯
sq_f_u : IsPullback (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := ⋯
f₁ : pullback f u ⟶ A := ⋯
l₂ : pullback f v ⟶ K := ⋯
f₂ : pullback f v ⟶ B := ⋯
m₁ : pullback g u ⟶ K := ⋯
g₁ : pullback g u ⟶ A := ⋯
m₂ : pullback g v ⟶ K := ⋯
g₂ : pullback g v ⟶ B := ⋯
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := ⋯
sq₁₁ : IsPullback (fst m₁ l₁) (snd m₁ l₁) m₁ l₁ := ⋯
sq₁₂ : IsPullback (fst m₁ l₂) (snd m₁ l₂) m₁ l₂ := ⋯
⊢ fst m₁ l₁ ≫ fst g u ≫ f = fst m₁ l₁ ≫ fst g u ≫ g

Tactic:
rw [pullback.condition_assoc, sq_f_u.w, sq_g_u.w, ← Category.assoc, ← Category.assoc]

Goal state after:
case h'_w.h'_w
J : Type v'
inst✝⁴ : Category.{u', v'} J
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✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this✝¹ : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
this✝ : Mono v := mono_of_isPushout_of_mono_left (of_hasPushout (fst a b) (snd a b))
sq_f_u : IsPullback (fst f u) (snd f u) f u := of_hasPullback f u
sq_f_v : IsPullback (fst f v) (snd f v) f v := of_hasPullback f v
sq_g_u : IsPullback (fst g u) (snd g u) g u := of_hasPullback g u
sq_g_v : IsPullback (fst g v) (snd g v) g v := of_hasPullback 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✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := Eq.mpr (id (congrArg (fun _a ↦ Mono _a) (Eq.symm (isoPullback_hom_fst p₁)))) inferInstance
sq₁₁ : IsPullback (fst m₁ l₁) (snd m₁ l₁) m₁ l₁ := of_hasPullback m₁ l₁
sq₁₂ : IsPullback (fst m₁ l₂) (snd m₁ l₂) m₁ l₂ := of_hasPullback m₁ l₂
⊢ (snd m₁ l₁ ≫ snd f u) ≫ u = (fst m₁ l₁ ≫ snd g u) ≫ u
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)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
⊢ PreservesLimitsOfShape K (plusPlusSheaf J D)

Tactic:
by
  let e := (FinCategory.equivAsType K).symm.trans (AsSmall.equiv.{0, 0, t})
  have : HasLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) D :=
    Limits.hasLimitsOfShape_of_equivalence e
  have : FinCategory (AsSmall.{t} (FinCategory.AsType K)) := by
    constructor
    · change Fintype (ULift _)
      infer_instance
    · intro j j'
      change Fintype (ULift _)
      infer_instance
  refine @preservesLimitsOfShape_of_equiv _ _ _ _ _ _ _ _ e.symm _ (show _ from ?_)
  constructor; intro F; constructor; intro S hS; constructor
  apply isLimitOfReflects (sheafToPresheaf J D)
  have : ReflectsLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) (forget D) :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms
  apply isLimitOfPreserves (J.sheafification D) hS

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : Adhesive D
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : F.ReflectsIsomorphisms
⊢ Adhesive C

Tactic:
have : ReflectsLimitsOfShape WalkingCospan F :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : Adhesive D
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ Adhesive C
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallyInjective J (J.toSheafify P)

Tactic:
dsimp [GrothendieckTopology.toSheafify]
  rw [GrothendieckTopology.plusMap_toPlus]
  infer_instance

Goal state after: