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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
⊢ x₁.IsAmalgamation (hP₁.amalgamate x₁ hx₁)

Tactic:
exact IsSheafFor.isAmalgamation hP₁ hx₁

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
H : J = ⊤
F : Sheaf J A
⊢ IsTerminal F

Tactic:
refine IsTerminal.isTerminalOfObj (sheafToPresheaf _ _) _ ?_
  refine Functor.isTerminal fun X ↦ Sheaf.isTerminalOfBotCover _ _ ?_
  simp [H]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x✝ : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
⊢ ∃ a, Arrows.toCompatible P π a = ⟨y, hy⟩

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
⊢ ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
· obtain ⟨x, hx, _⟩ := h y hy
    exact ⟨x, by ext; apply hx⟩

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
⊢ ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
⊢ homOfLe ⋯ ≫ G.sheafifyLift f h = f

Tactic:
ext U s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
⊢ (ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s = (ConcreteCategory.hom (f.app U)).toFun s
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
⊢ l₁ = l₂

Tactic:
ext U s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
⊢ (ConcreteCategory.hom (l₁.app U)).toFun s = (ConcreteCategory.hom (l₂.app U)).toFun s
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
A : (J.Cover X)ᵒᵖ
⊢ ∀ {Y : (J.Cover X)ᵒᵖ} (f : A ⟶ Y),
    (J.diagram P X ⋙ F).map f ≫
        ((isLimitOfPreserves F (limit.isLimit ((unop Y).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop Y).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop Y)).symm).hom =
      ((isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop A).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm).hom ≫
        (J.diagram (P ⋙ F) X).map f

Tactic:
B

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
A B : (J.Cover X)ᵒᵖ
⊢ ∀ (f : A ⟶ B),
    (J.diagram P X ⋙ F).map f ≫
        ((isLimitOfPreserves F (limit.isLimit ((unop B).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop B).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop B)).symm).hom =
      ((isLimitOfPreserves F (limit.isLimit ((unop A).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop A).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop A)).symm).hom ≫
        (J.diagram (P ⋙ F) X).map f
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
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)
hT : t.Compatible
Z Y : C
f : Z ⟶ Y
g : Y ⟶ X
hg : U.arrows g
hf : (B hg).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) (t g hg) = s (f ≫ g) ⋯

Tactic:
apply ht hg _ hf

Goal state after:
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
FD : D → D → Type u_3
CD : D → Type u_4
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
⊢ (J.sheafifyCompIso F P).inv = J.sheafifyLift (whiskerRight (J.toSheafify P) F) ⋯

Tactic:
by
  apply J.sheafifyLift_unique
  rw [Iso.comp_inv_eq]
  simp

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
⊢ ∃ t, Meq.mk S t = s

Tactic:
by
  have inj : ∀ X : C, Function.Injective ((J.toPlus P).app (op X)) := inj_of_sep _ hsep
  -- Choose representatives for the given local sections.
  choose T t ht using fun I => exists_rep (s I)
  -- Construct a large cover over which we will define a representative that will
  -- provide the gluing of the given local sections.
  let B : J.Cover X := S.bind T
  choose Z e1 e2 he2 _ _ using fun I : B.Arrow => I.hf
  -- Construct a compatible system of local sections over this large cover, using the chosen
  -- representatives of our local sections.
  -- The compatibility here follows from the separatedness assumption.
  let w : Meq P B := meqOfSep P hsep X S s T t ht
  -- The associated gluing will be the candidate section.
  use mk w
  ext I
  dsimp [Meq.mk]
  rw [ht, res_mk_eq_mk_pullback]
  -- Use the separatedness of `P⁺` to prove that this is indeed a gluing of our
  -- original local sections.
  apply sep P (T I)
  intro II
  simp only [res_mk_eq_mk_pullback, eq_mk_iff_exists]
  -- It suffices to prove equality for representatives over a
  -- convenient sufficiently large cover...
  use (J.pullback II.f).obj (T I)
  let e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) :=
    homOfLE
      (by
        intro Y f hf
        apply Sieve.le_pullback_bind _ _ _ I.hf
        · cases I
          exact hf)
  use e0, 𝟙 _
  ext IV
  let IA : B.Arrow := ⟨_, (IV.f ≫ II.f) ≫ I.f,
    ⟨I.Y, _, _, I.hf, Sieve.downward_closed _ II.hf _, rfl⟩⟩
  let IB : S.Arrow := IA.fromMiddle
  let IC : (T IB).Arrow := IA.toMiddle
  let ID : (T I).Arrow := ⟨IV.Y, IV.f ≫ II.f, Sieve.downward_closed (T I).1 II.hf IV.f⟩
  change t IB IC = t I ID
  apply inj IV.Y
  rw [toPlus_apply (T I) (t I) ID]
  erw [toPlus_apply (T IB) (t IB) IC]
  rw [← ht, ← ht]
  -- Conclude by constructing the relation showing equality...
  let IR : S.Relation := { fst.hf := IB.hf, snd.hf := I.hf, r.w := IA.middle_spec, .. }
  exact s.condition IR

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

Goal state before:
pp: case right
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 : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
⊢ ∃ a, (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) a = x

Tactic:
use t

Goal state after:
case h
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 : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
⊢ (ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) t = x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g)) →
    y ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mp
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑(pullback f g)
⊢ (ConcreteCategory.hom (pullback.snd f g)) x ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
⊢ IsVanKampenColimit c'

Tactic:
intro F' c'' α f h hα
  have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
    ext j
    exact e.inv.2 j
  rw [H c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα]
  apply forall_congr'
  intro j
  conv_lhs => rw [← Category.comp_id (α.app j)]
  have : IsIso e.inv.hom := Functor.map_isIso (Cocone.forget _) e.inv
  exact (IsPullback.of_vert_isIso ⟨by simp⟩).paste_vert_iff (NatTrans.congr_app h j).symm

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

Goal state before:
pp: case e_a
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
i j : J
g : i ⟶ j
⊢ Gr.map (F.map g) ≫ c.ι.app j = c.ι.app i

Tactic:
exact c.w _

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case pos
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))
x : Z
hx : (ConcreteCategory.hom f) (x, PUnit.unit).1 = (ConcreteCategory.hom (↾Sum.inr)) (x, PUnit.unit).2
h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit
⊢ (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩) = (ConcreteCategory.hom s.inr) ⟨(x, PUnit.unit), hx⟩

Tactic:
cases h.symm.trans hx

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case a
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} ⊕ PUnit.{u + 1})
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl))

Tactic:
· rintro x ⟨⟨⟩, hx⟩; refine ⟨⟨⟨x, PUnit.unit⟩, hx.symm⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case a
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} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr ⊆
    Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr))

Tactic:
· rintro x ⟨⟨⟩, hx⟩; refine ⟨⟨⟨x, PUnit.unit⟩, hx.symm⟩, rfl⟩

Goal state after:
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)
O : Finset K := (Finset.univ.biUnion fun j ↦ Finset.univ.biUnion fun j' ↦ Finset.image kf Finset.univ) ∪ {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
k'O : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun j ↦
    Finset.univ.biUnion fun j' ↦
      Finset.univ.biUnion fun f ↦ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ True

Tactic:
trivial

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
⊢ ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (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)

Tactic:
introv hX hY

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
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
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Sheaf J RingCat
F : D ⥤ SheafOfModules R
inst✝¹ :
  ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj.obj X))).sections
inst✝ : HasLimitsOfShape D AddCommGrpCat
X : Cᵒᵖ
⊢ PreservesLimit F (evaluation R X)

Tactic:
dsimp [evaluation]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case coe
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
d : ℕ∞
hd : projectiveDimension X = ↑d
⊢ ↑d ≠ ⊤ ↔ ∃ n, HasProjectiveDimensionLE X n

Tactic:
induction d with
    | top =>
      by_contra!
      simp only [WithBot.coe_top, ne_eq, not_true_eq_false, false_and, true_and, false_or] at this
      obtain ⟨n, hn⟩ := this
      rw [← projectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn
      exact ENat.natCast_ne_top _ ((WithBot.coe_eq_coe).1 hn)
    | coe d =>
      simp only [ne_eq, WithBot.coe_eq_top, ENat.natCast_ne_top, not_false_eq_true, true_iff]
      exact ⟨d, by simpa only [← projectiveDimension_le_iff] using! hd.le⟩

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (mapComp (f ≫ g) h).hom ≫
        (mapComp f g).hom ▷ map h ≫
          (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
      eqToHom ⋯
map₂_left_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ c✝ : B
x✝² : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ eqToHom ⋯ = (mapComp x✝² x✝¹).hom ≫ map x✝² ◁ eqToHom ⋯ ≫ (mapComp x✝² x✝).inv

Tactic:
by
    obtain rfl := obj_ext_of_isDiscrete η
    simp

Goal state after: