mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ η = γ

Tactic:
rw [this]

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.plusLift (J.toPlus P ≫ γ) hQ
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case mp
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)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
⊢ mk x = mk y → ∃ W h1 h2, x.refine h1 = y.refine h2

Tactic:
intro h
    obtain ⟨W, h1, h2, hh⟩ := Concrete.colimit_exists_of_rep_eq (C := D) _ _ _ h
    use W.unop, h1.unop, h2.unop
    ext I
    apply_fun Multiequalizer.ι (W.unop.index P) I at hh
    convert! hh
    all_goals
      dsimp [diagram]
      rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
      erw [Meq.equiv_symm_eq_apply]
      cases I; rfl

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)),
      ((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))

Tactic:
FamilyOfElements.isAmalgamation_singleton_iff,

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₁ = (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))
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)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            (ConcreteCategory.hom (P.map p₁.op)) ((FamilyOfElements.singletonEquiv P f).symm b f ⋯) =
              (ConcreteCategory.hom (P.map p₂.op)) ((FamilyOfElements.singletonEquiv P f).symm b f ⋯)) →
        ∃! 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

Tactic:
FamilyOfElements.isAmalgamation_singleton_iff,

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)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            (ConcreteCategory.hom (P.map p₁.op)) ((FamilyOfElements.singletonEquiv P f).symm b f ⋯) =
              (ConcreteCategory.hom (P.map p₂.op)) ((FamilyOfElements.singletonEquiv P f).symm b f ⋯)) →
        ∃! t, (ConcreteCategory.hom (P.map f.op)) t = (FamilyOfElements.singletonEquiv P f).symm b f ⋯) ↔
    ∀ (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.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (ConcreteCategory.hom (F.map (i.op ≫ i'.op))) ↑s = x'' (i' ≫ i) hi''
⊢ (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
    (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)

Tactic:
F.map_comp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (ConcreteCategory.hom (F.map i.op ≫ F.map i'.op)) ↑s = x'' (i' ≫ i) hi''
⊢ (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
    (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop V⦄,
    (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows f_1 →
      (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom
                ((sheafify J G).toFunctor.map i ≫
                  ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)).toFun
            s) =
        (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom ((↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i)).toFun
            s)

Tactic:
intro W j hj

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj : (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j
⊢ (ConcreteCategory.hom (F'.map j.op))
      ((ConcreteCategory.hom
            ((sheafify J G).toFunctor.map i ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)).toFun
        s) =
    (ConcreteCategory.hom (F'.map j.op))
      ((ConcreteCategory.hom ((↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i)).toFun s)
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
⊢ J.plusFunctor D ⋙ (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.plusFunctor E ≅
    (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.sheafification E

Tactic:
refine ?_ ≪≫ associator _ _ _

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
⊢ J.plusFunctor D ⋙ (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.plusFunctor E ≅
    ((whiskeringRight Cᵒᵖ D E).obj F ⋙ J.plusFunctor E) ⋙ J.plusFunctor E
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case trans
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S) = Sieve.pullback f R
⊢ IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S)).arrows

Tactic:
rw [this]

Goal state after:
case trans
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S) = Sieve.pullback f R
⊢ IsSeparatedFor P (Sieve.pullback f R).arrows
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) ≫
        (W.multifork E.pt).ι i) ≫
      (((evaluation Cᵒᵖ D).obj (op i.Y)).mapCone E).π.app k =
    S.ι i ≫ (((evaluation Cᵒᵖ D).obj (op i.Y)).mapCone E).π.app k

Tactic:
dsimp [Multifork.ofι]

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 =
    (Multifork.ofι (W.index (F.obj k).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) ⋯).ι i

Tactic:
dsimp [Multifork.ofι]

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 =
    Multifork.ι
      { pt := S.pt,
        π :=
          {
            app := fun x ↦
              match x with
              | WalkingMulticospan.left a => S.ι a ≫ (E.π.app k).app (op a.Y)
              | WalkingMulticospan.right b => (S.ι b.fst ≫ (E.π.app k).app (op b.fst.Y)) ≫ (F.obj k).obj.map b.r.g₁.op,
            naturality := ⋯ } }
      i
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
rw [this, CategoryTheory.mono_iff_injective]
    rfl

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 : Cocone (Discrete.functor β)
j : Discrete ι
⊢ (sigmaCofan β).ι.app j ≫
      ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ } =
    s.ι.app j

Tactic:
by
    cases j
    cat_disch

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst f g

Tactic:
by
  rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_fst]

Goal state after:
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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
this : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
⊢ Mono inl

Tactic:
rw [this]

Goal state after:
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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
this : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
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₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono inr

Tactic:
rw [this]

Goal state after:
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₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inr
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.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : Y'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inl y

Tactic:
apply_fun f at h

Goal state after:
case inr
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.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : Y'✝
h : (ConcreteCategory.hom f) ((ConcreteCategory.hom s.fst) x) = (ConcreteCategory.hom f) (Sum.inr val)
⊢ ∃! y, Sum.inr val = Sum.inl y
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inl
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}))
x : s.pt
val : X'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inr y

Tactic:
apply_fun f at h

Goal state after:
case inl
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}))
x : s.pt
val : X'✝
h : (ConcreteCategory.hom f) ((ConcreteCategory.hom s.fst) x) = (ConcreteCategory.hom f) (Sum.inl val)
⊢ ∃! y, Sum.inl val = Sum.inr y
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

Tactic:
rw [← H.w_assoc]

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
⊢ f ≫ iY ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inr
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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inl y

Tactic:
apply_fun f at h

Goal state after:
case inr
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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom f) ((ConcreteCategory.hom s.fst) x) = (ConcreteCategory.hom f) (Sum.inr val)
⊢ ∃! y, Sum.inr val = Sum.inl y