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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
⊢ f = g

Tactic:
ext Y y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f✝ : Y✝ ⟶ X
S R : Sieve X
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
Y : Cᵒᵖ
y : Z✝.obj Y
⊢ (hom (f.app Y)).toFun y = (hom (g.app Y)).toFun y
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R S : Sieve X
Z✝ : Cᵒᵖ ⥤ Type (max w v₁)
x✝¹ x✝ : Z✝ ⟶ S.uliftFunctor
h : x✝¹ ≫ S.uliftFunctorInclusion = x✝ ≫ S.uliftFunctorInclusion
⊢ x✝¹ = x✝

Tactic:
ext Y y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
S✝ R S : Sieve X
Z✝ : Cᵒᵖ ⥤ Type (max w v₁)
x✝¹ x✝ : Z✝ ⟶ S.uliftFunctor
h : x✝¹ ≫ S.uliftFunctorInclusion = x✝ ≫ S.uliftFunctorInclusion
Y : Cᵒᵖ
y : Z✝.obj Y
⊢ (hom (x✝¹.app Y)).toFun y = (hom (x✝.app Y)).toFun y
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X✝ : C
R : Presieve X✝
S : Sieve X✝
inst✝ : R.HasPairwisePullbacks
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ F.map f.op ≫ F.map c.fst.op = F.map f.op ≫ F.map c.snd.op

Tactic:
by simp [← Functor.map_comp, ← op_comp, c.condition]

Goal state after:
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
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
S : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap 0).app x✝ = colimit.ι (J.diagram P (unop x✝)) S ≫ NatTrans.app 0 x✝

Tactic:
simp [plusMap]

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
⊢ (∀ (x : FamilyOfElements P (singleton f)) (t₁ t₂ : P.obj (op Y)),
      x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))

Tactic:
Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)

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)),
      ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₁ →
        ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₂ → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))
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
⊢ (∀ (x : FamilyOfElements P (singleton f)), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) x = (ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (P.map f.op)) y = x

Tactic:
Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)

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)),
      ((FamilyOfElements.singletonEquiv P f).symm b).Compatible →
        ∃! t, ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) x = (ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (P.map f.op)) y = x
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
⊢ ∀ ⦃f_1 : M ⟶ Y⦄,
    (Sieve.pullback (l ≫ h) (B hf)).arrows f_1 →
      (ConcreteCategory.hom (P.map f_1.op)) ((ConcreteCategory.hom (P.map l.op)) (t (h ≫ f) ⋯)) =
        (ConcreteCategory.hom (P.map f_1.op))
          ((ConcreteCategory.hom (P.map l.op)) ((ConcreteCategory.hom (P.map h.op)) (t f hf)))

Tactic:
m

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
⊢ (Sieve.pullback (l ≫ h) (B hf)).arrows m →
    (ConcreteCategory.hom (P.map m.op)) ((ConcreteCategory.hom (P.map l.op)) (t (h ≫ f) ⋯)) =
      (ConcreteCategory.hom (P.map m.op))
        ((ConcreteCategory.hom (P.map l.op)) ((ConcreteCategory.hom (P.map h.op)) (t f hf)))
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),
    (∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i) →
      m = (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S)

Tactic:
m

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
⊢ (∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i) →
    m = (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
ι : Type u_5
inst✝ : Category.{v_2, u_3} C
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i }) (α.app { as := i }) (𝟙 (G.obj { as := i }))

Tactic:
exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
inst✝ : Category.{v_2, u_3} C
ι : Type u_6
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i }) (α.app { as := i }) (𝟙 (G.obj { as := i }))

Tactic:
exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Goal state after:
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 i ↦ (ConcreteCategory.hom (S.π.app { as := i })) s, continuous_toFun := ⋯ }

Tactic:
m

Goal state after:
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 i ↦ (ConcreteCategory.hom (S.π.app { as := i })) s, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
⊢ ∀ (m : (sigmaCofan β).pt ⟶ S.pt),
    (∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = S.ι.app j) →
      m = ofHom { toFun := fun s ↦ (ConcreteCategory.hom (S.ι.app { as := s.fst })) s.snd, continuous_toFun := ⋯ }

Tactic:
m

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
m : (sigmaCofan β).pt ⟶ S.pt
⊢ (∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = S.ι.app j) →
    m = ofHom { toFun := fun s ↦ (ConcreteCategory.hom (S.ι.app { as := s.fst })) s.snd, continuous_toFun := ⋯ }
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)
⊢ ∀ (m : S.pt ⟶ (X.prodBinaryFan Y).pt),
    (∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j) →
      m =
        ofHom
          { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
            continuous_toFun := ⋯ }

Tactic:
m

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
⊢ (∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j) →
    m =
      ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ }
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:
m

Goal state after:
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 := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case e'_5
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
e_1✝ : ↑(range ⇑(ConcreteCategory.hom c.inl))ᶜ = { a // a ∉ range ⇑(ConcreteCategory.hom c.inl) }
⊢ ((range ⇑(ConcreteCategory.hom c.inl))ᶜ.domRestrict fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑⋯.toHomeomorph.symm ∘ Subtype.map (fun a ↦ a) this

pp: case neg
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous (⇑(ConcreteCategory.hom g) ∘ ⇑⋯.toHomeomorph.symm ∘ Subtype.map (fun a ↦ a) this)

Tactic:
· ext ⟨x, hx⟩
              exact dif_neg hx

Goal state after:
case neg
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous (⇑(ConcreteCategory.hom g) ∘ ⇑⋯.toHomeomorph.symm ∘ Subtype.map (fun a ↦ a) this)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan (X ∘ Sum.inl)
c₂ : Cofan (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst✝ : MonoCoprod C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
⊢ inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
exact Cofan.IsColimit.hom_ext hc₂ _ _ (by simpa using hinr)

Goal state after:
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
⊢ {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:
intro Z f

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
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))
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₂.uniq
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
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
⊢ ∀ (m : Z ⟶ s.pt),
    (↾fun p ↦ (↑p).1) ≫ m = s.inl →
      (↾fun p ↦ (↑p).1) ≫ m = s.inr →
        m =
          ↾fun x ↦
            if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
            else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)

Tactic:
m

Goal state after:
case h₂.uniq
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
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
m : Z ⟶ s.pt
⊢ (↾fun p ↦ (↑p).1) ≫ m = s.inl →
    (↾fun p ↦ (↑p).1) ≫ m = s.inr →
      m =
        ↾fun x ↦
          if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
          else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.uniq
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 : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ ∀ (m : YE ⟶ s.pt),
    (c.inr ≫ fE) ≫ m = s.inl →
      iY ≫ m = s.inr → m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
m

Goal state after:
case mpr.uniq
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 : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
⊢ (c.inr ≫ fE) ≫ m = s.inl →
    iY ≫ m = s.inr → m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
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
⊢ {Z : TopCat} →
    (f : Z ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt) →
      IsColimit
        (BinaryCofan.mk
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl).fst
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr).fst)

Tactic:
intro Z f

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
Z : TopCat
f : Z ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
⊢ IsColimit
    (BinaryCofan.mk (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl).fst
      (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr).fst)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: 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)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j) =
    (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f ≫ i f))) (y j)

Tactic:
by
            rw [s (𝟙 j) f]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ ∀ (X Y : Discrete (Fin n)) (f_1 : X ⟶ Y), F.map f_1 ≍ (Discrete.functor f).map f_1

Tactic:
by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ ∀ (X Y : Discrete (Fin n)) (f_1 : X ⟶ Y), F.map f_1 ≍ (Discrete.functor f).map f_1

Tactic:
by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj i
f : ι → C := F.obj ∘ Discrete.mk
⊢ ∀ (X Y : Discrete ι) (f_1 : X ⟶ Y), F.map f_1 ≍ (Discrete.functor f).map f_1

Tactic:
by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f]

Goal state after:
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),
    (∀ (j : K),
        m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j) →
      m = liftToDiagramLimitObj F E

Tactic:
m

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
⊢ (∀ (j : K),
      m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j) →
    m = liftToDiagramLimitObj F E