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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows) →
    ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)

Tactic:
rintro h ⟨E, π⟩

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone S.arrows.cocone.op)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
hf : S.arrows f
x : unop (op X)
⊢ (ConcreteCategory.hom (P.map f.op)) (⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯) =
    (ConcreteCategory.hom (z f hf)) x

Tactic:
apply Presieve.IsSheafFor.valid_glue

Goal state after:
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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
i : (S.pullback f).Arrow
⊢ ↑x i.base = ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }

Tactic:
cases i

Goal state after:
case mk
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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
Y✝ : C
f✝ : Y✝ ⟶ Y
hf✝ : (↑(S.pullback f)).arrows f✝
⊢ ↑x { Y := Y✝, f := f✝, hf := hf✝ }.base =
    ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
⊢ IsSeparatedFor P' R

Tactic:
intro x t₁ t₂ ht₁ ht₂
  simpa using congrArg (i.hom.app _) <| hP (x.map i.inv) _ _ (ht₁.map i.inv) (ht₂.map i.inv)

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

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
use hS.amalgamate _ (hx.restrict h)

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
⊢ x.IsAmalgamation (hS.amalgamate (FamilyOfElements.restrict h x) ⋯)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2
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
j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })
⊢ ((parallelPair (s.map (firstMap R P)) (s.map (secondMap R P))).map WalkingParallelPairHom.right ≫
        (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))).hom) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j =
    ((PreservesProduct.iso s fun f ↦ P.obj (op f.fst)).hom ≫
        (parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R)).map
          WalkingParallelPairHom.right) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j

Tactic:
· dsimp [Equalizer.Presieve.secondMap, secondMap]
      simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt,
        Fan.mk_π_app, assoc, piComparison_comp_π_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor P (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i)) ↔
    IsSheafFor P (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows

Tactic:
isSheafFor_iff_generate

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor P (generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i))).arrows ↔
    IsSheafFor P (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows
Module: Mathlib.CategoryTheory.Subfunctor.Sieves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map g₁.op)) ((ConcreteCategory.hom (F.map f₁.op)) s) =
    (ConcreteCategory.hom (F.map g₂.op)) ((ConcreteCategory.hom (F.map f₂.op)) s)

Tactic:
rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp, ← op_comp, ← op_comp, e]

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

Goal state before:
pp: case e'_2
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
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ ↑x (Cover.Arrow.map i h1) = ↑x { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
cases i

Goal state after:
case e'_2.mk
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
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop (op S))).arrows f✝
e : ↑(x.refine h1) { Y := Y✝, f := f✝, hf := hf✝ } = ↑(y.refine h2) { Y := Y✝, f := f✝, hf := hf✝ }
e_1✝ :
  CD (((unop (op S)).index P).left { Y := Y✝, f := f✝, hf := hf✝ }) =
    ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y))
⊢ ↑x ({ Y := Y✝, f := f✝, hf := hf✝ }.map h1) =
    ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_3
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
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ ↑y (Cover.Arrow.map i h2) = ↑y { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
cases i

Goal state after:
case e'_3.mk
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
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop (op S))).arrows f✝
e : ↑(x.refine h1) { Y := Y✝, f := f✝, hf := hf✝ } = ↑(y.refine h2) { Y := Y✝, f := f✝, hf := hf✝ }
e_1✝ :
  CD (((unop (op S)).index P).left { Y := Y✝, f := f✝, hf := hf✝ }) =
    ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y))
⊢ ↑y ({ Y := Y✝, f := f✝, hf := hf✝ }.map h2) =
    ↑y { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { obj := P, property := hP }) ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { obj := P, property := hP }) =
    𝟙 (sheafify J P)

Tactic:
rw [← (sheafificationAdjunction J D).inv_counit_map (X := ⟨P, hP⟩)]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { obj := P, property := hP }) ≫
      inv ((sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { obj := P, property := hP })) =
    𝟙 (sheafify J P)
Module: Mathlib.CategoryTheory.Sites.Sheafification

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

Tactic:
sheafifyLift_unique J _ hQ _ h,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ sheafifyLift J (toSheafify J P ≫ γ) hQ = γ
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
P : Cᵒᵖ ⥤ D
h : ObjectProperty.LimitOfShape (Presheaf.IsSheaf J) K P
F : K ⥤ Sheaf J D := ObjectProperty.lift (Presheaf.IsSheaf J) h.diag ⋯
⊢ Presheaf.IsSheaf J P

Tactic:
exact isSheaf_of_isLimit F _ h.isLimit

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

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

Tactic:
· specialize h ⟨WalkingPair.right⟩
      apply_fun fun e => e x at h
      exact h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
x : (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).pt
⊢ T✝

Tactic:
by
          rcases x with x | x
          exacts [f₁ x, f₂ x]

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₂
T✝ : C
f₁ : c₁.pt ⟶ T✝
f₂ : c₂.pt ⟶ T✝
m : (binaryCofanSum c c₁ c₂ hc₁ hc₂).pt ⟶ T✝
hm₁ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl ≫ m = f₁
hm₂ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr ≫ m = f₂
⊢ m =
    Cofan.IsColimit.desc hc fun i ↦
      match i with
      | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
      | Sum.inr i₂ => c₂.inj i₂ ≫ f₂

Tactic:
apply Cofan.IsColimit.hom_ext hc

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₂
T✝ : C
f₁ : c₁.pt ⟶ T✝
f₂ : c₂.pt ⟶ T✝
m : (binaryCofanSum c c₁ c₂ hc₁ hc₂).pt ⟶ T✝
hm₁ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl ≫ m = f₁
hm₂ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr ≫ m = f₂
⊢ ∀ (i : I₁ ⊕ I₂),
    c.inj i ≫ m =
      c.inj i ≫
        Cofan.IsColimit.desc hc fun i ↦
          match i with
          | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
          | Sum.inr i₂ => c₂.inj i₂ ≫ f₂
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₂)
⊢ ∀ (i : I₂), c₂.inj i ≫ inr = c₂.inj i ≫ (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
by simpa using hinr

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

Goal state before:
pp: 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
i : WalkingPair
⊢ Mono (Cofan.inj c i)

Tactic:
cases i

Goal state after:
case left
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.left)

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)
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case e'_4
C : Type u
inst✝ : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint X Y
X : WalkingPair → C
x✝ : WalkingPair
⊢ X x✝ = WalkingPair.casesOn x✝ (X WalkingPair.left) (X WalkingPair.right)

Tactic:
casesm WalkingPair <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
x : C
⊢ IsLimit (PullbackCone.mk (((evaluation C D).obj x).map (c'.ι.app j)) (((evaluation C D).obj x).map (α.app j)) ⋯)

Tactic:
exact ((this x).mp ⟨isColimitOfPreserves _ hc'⟩ _).isLimit

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
f : Fin 0 → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
exact isVanKampenColimit_of_isEmpty _ hc

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (Cofan.mk (∐ fun i ↦ f i.succ) (Sigma.ι fun i ↦ f i.succ))

Tactic:
apply IH
      exact coproductIsCoproduct _

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsVanKampenColimit c

Tactic:
apply (IsVanKampenColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u''
inst✝² : Category.{v'', u''} D
X✝ Y✝ : C
inst✝¹ : FinitaryPreExtensive C
X Z : C
α : Type u_1
f : X ⟶ Z
Y : α → C
i : (a : α) → Y a ⟶ Z
inst✝ : Finite α
hi : IsIso (Sigma.desc i)
a : α
⊢ HasPullback f (i a)

Tactic:
by
  apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct (c := Cofan.mk Z i)
  exact @IsColimit.ofPointIso (t := Cofan.mk Z i) (P := _) (i := hi)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) (adj.unit.app X)

Tactic:
by
  rintro _ ⟨Y, rfl⟩
  convert!
    ((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans
        (adj.homEquiv X Y)).bijective using 1
  dsimp [Adjunction.homEquiv]
  aesop

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ (isColocal fun x ↦ x ∈ Set.range G.obj) = (MorphismProperty.isomorphisms D).inverseImage F

Tactic:
by
  ext P₁ P₂ f
  rw [isColocal_iff_isIso_map adj]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
· ext ⟨⟨⟩⟩ <;> simp

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (const (Discrete WalkingPair)).map c.inr

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
· ext ⟨⟨⟩⟩ <;> simp

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mp
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
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x y : ToType (F.obj X)
⊢ equalizerSieve x y = ⊤ → x = y

Tactic:
intro h
    simpa using (show equalizerSieve x y (𝟙 _) by simp [h])

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app X)) a = s

Tactic:
let t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
      fun Y g hg => Presheaf.localPreimage f.hom s g hg

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app X)) a = s