mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ IsConnected C ↔ IsConnected D

Tactic:
by
  rw [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} C,
    isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} D]
  exact Equiv.nonempty_congr <| Iso.isoCongrLeft <|
    CategoryTheory.Functor.Final.colimitIso F <| constPUnitFunctor.{max u v u₂ v₂} D

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
⊢ IsConnected C

Tactic:
rw [Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
⊢ Nonempty (colimit (Types.constPUnitFunctor C) ≅ PUnit.{(max u ?u.35) + 1})
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s =
    (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s'
c' : C
t₁ t₂ : c ⟶ c'
h :
  (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₁)) s =
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₂)) s'
| s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂)

Tactic:
rw [IsFiltered.coeq_condition t₁ t₂]

Goal state after:
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s =
    (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s'
c' : C
t₁ t₂ : c ⟶ c'
h :
  (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₁)) s =
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₂)) s'
| s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂)
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ 𝟙 (F.1 Y) ≫ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j') =
    F.partialRightAdjointHomEquiv (f ≫ c'.π.app j) ≫ (R.map φ).hom

Tactic:
rw [id_comp, ← c'.w φ, ← partialRightAdjointHomEquiv_map_comp,
              ← assoc]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ (R ⋙ F.partialRightAdjoint).map φ) =
    F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ F.partialRightAdjointMap (R.map φ))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (f.app Y)) ((ConcreteCategory.hom (M₁.map φ)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (g.app Y)) ((ConcreteCategory.hom (M₃.map φ)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)

Tactic:
rw [naturality_apply, naturality_apply]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (M₂.map φ)) ((ConcreteCategory.hom (f.app X)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ConcreteCategory.hom (g.app X)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)
Module: Mathlib.CategoryTheory.Sites.Precoverage

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
X : C
R : Presieve X
inst✝¹ : F.PreservesPairwisePullbacks R
inst✝ : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
x✝¹ : map F R f
g : Z ⟶ F.obj X
x✝ : map F R g
Y✝¹ : C
u✝¹ : Y✝¹ ⟶ X
hf : R u✝¹
Y✝ : C
u✝ : Y✝ ⟶ X
hg : R u✝
⊢ HasPullback (F.map u✝¹) (F.map u✝)

Tactic:
have := Presieve.HasPairwisePullbacks.has_pullbacks hf hg

Goal state after:
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
X : C
R : Presieve X
inst✝¹ : F.PreservesPairwisePullbacks R
inst✝ : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
x✝¹ : map F R f
g : Z ⟶ F.obj X
x✝ : map F R g
Y✝¹ : C
u✝¹ : Y✝¹ ⟶ X
hf : R u✝¹
Y✝ : C
u✝ : Y✝ ⟶ X
hg : R u✝
this : HasPullback u✝¹ u✝
⊢ HasPullback (F.map u✝¹) (F.map u✝)
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m✝ : s.pt ⟶ (Fork.ofι (↾Subtype.val) ⋯).pt
hm : m✝ ≫ (Fork.ofι (↾Subtype.val) ⋯).ι = s.ι
x : s.pt
⊢ (hom m✝).toFun x = (hom (↾fun i ↦ ⟨(hom s.ι) i, ⋯⟩)).toFun x

Tactic:
exact Subtype.ext (by exact congr_hom hm x)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
⊢ (pullbackArrows b s).uncurry = (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

Tactic:
ext ⟨Z, v⟩; constructor
  · rintro ⟨Y, u, hu⟩; exact ⟨⟨Y, u⟩, hu, rfl⟩
  · rintro ⟨⟨Y, u⟩, hu, h⟩
    rw [Sigma.ext_iff] at h
    obtain ⟨rfl, h⟩ := h
    rw [heq_iff_eq] at h; subst h
    exact ⟨Y, u, hu⟩

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd⟩ ∈
    (s.bind t).uncurry

Tactic:
exact ⟨_, _, _, _, hg, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ generate R = ⊤

Tactic:
by
  rw [← id_mem_iff_eq_top]
  exact ⟨_, section_ f, f, hf, by simp⟩

Goal state after:
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✝
I : Type u_1
Y : I → C
X : C
⊢ ∀ {Y_1 Z : C} {f : Y_1 ⟶ X}, (∃ i, Nonempty (Y_1 ⟶ Y i)) → ∀ (g : Z ⟶ Y_1), ∃ i, Nonempty (Z ⟶ Y i)

Tactic:
rintro Z₁ Z₂ p ⟨i, ⟨f⟩⟩ g
    exact ⟨i, ⟨g ≫ f⟩⟩

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, (hom (↾fun f ↦ ↑f)) t = f✝

Tactic:
· intro hf
    exact ⟨⟨_, hf⟩, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible P fun i ↦ (Over.map p).map (f i))
i₁ i₂ : I
Z : Over B
g₁ : Z ⟶ Y i₁
g₂ : Z ⟶ Y i₂
h : g₁ ≫ f i₁ = g₂ ≫ f i₂
⊢ (Over.map p).map g₁ ≫ (fun i ↦ (Over.map p).map (f i)) i₁ = (Over.map p).map g₂ ≫ (fun i ↦ (Over.map p).map (f i)) i₂

Tactic:
simp only [← Functor.map_comp, h]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EpiMono

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

Tactic:
this,

Goal state after:
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Epi ((forget TopCat).map f) ↔ Function.Surjective ⇑(ConcreteCategory.hom f)
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:
this,

Goal state after:
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Mono ((forget TopCat).map f) ↔ Function.Injective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
coinduced_le_iff_le_induced,

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
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
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ J.toSheafify P ≫ J.sheafifyLift η hQ = η

Tactic:
by
  dsimp only [sheafifyLift, toSheafify]
  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✝⁴ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram (J.plusObj F) (unop x✝)) j ≫ ((plusPlusSheaf J D).map 0).hom.app x✝ =
    colimit.ι (J.diagram (J.plusObj F) (unop x✝)) j ≫ (InducedCategory.Hom.hom 0).app x✝

Tactic:
erw [colimit.ι_map, comp_zero]

Goal state after:
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✝⁴ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j : (J.Cover (unop x✝))ᵒᵖ
⊢ (J.diagramNatTrans (J.plusMap 0) (unop x✝)).app j ≫ colimit.ι (J.diagram (J.plusObj G) (unop x✝)) j = 0
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
coinduced_le_iff_le_induced,

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
x : ↑S.1
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x).1 =
    (ConcreteCategory.hom g) ((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x).2

Tactic:
simpa using! ConcreteCategory.congr_hom S.condition x

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₁ := 𝟙 X) f g f (𝟙 _)
        (homeoOfIso (Iso.refl _)).isOpenEmbedding H (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ i ∧ IsPullback i' αY αZ h

Tactic:
simpa only [IsPushout.flip_iff, IsPullback.flip_iff, and_comm] using
    H' g' f' i' h' αW αY αX αZ hg hf hi hh w.flip

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
this : F = Discrete.functor f
⊢ IsUniversalColimit c

Tactic:
clear_value f

Goal state after:
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
this : F = Discrete.functor f
⊢ IsUniversalColimit c
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
this : F = Discrete.functor f
⊢ IsVanKampenColimit c

Tactic:
clear_value f

Goal state after:
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
this : F = Discrete.functor f
⊢ IsVanKampenColimit c
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
this : F = Discrete.functor f
⊢ HasPullback g (c.ι.app i)

Tactic:
clear_value f

Goal state after:
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
this : F = Discrete.functor f
⊢ HasPullback g (c.ι.app i)
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case refine_1
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
⊢ ∀ (s : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X)) (j : K),
    liftToPlusObjLimitObj F (unop X) s ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j =
      s.π.app j

Tactic:
intro S k
    apply liftToPlusObjLimitObj_fac

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)
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹⁰ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁹ : ConcreteCategory D FD
inst✝⁸ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁷ : (forget D).ReflectsIsomorphisms
inst✝⁶ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁵ : SmallCategory K
inst✝⁴ : FinCategory K
inst✝³ : HasLimitsOfShape K D
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
inst✝ : HasFiniteLimits D
⊢ PreservesFiniteLimits (plusPlusSheaf J D)

Tactic:
by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{t}
  intros
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Local

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective ((fun g ↦ f ≫ g) ∘ ⇑e.homToEquiv)

Tactic:
convert! (Iso.homToEquiv e).bijective.comp (hZ f hf) using 1

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ (fun g ↦ f ≫ g) ∘ ⇑e.homToEquiv = ⇑e.homToEquiv ∘ fun g ↦ f ≫ g
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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isLocal f
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective fun g_1 ↦ g ≫ g_1

Tactic:
rw [← Function.Bijective.of_comp_iff' (hf Z hZ)]
    simpa using! hfg Z hZ

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 Y : D
f : X ⟶ Y
this : f ≫ adj.unit.app Y = adj.unit.app X ≫ F.map (G.map f)
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) (f ≫ adj.unit.app Y) ↔ IsIso (G.map f)

Tactic:
this,

Goal state after:
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 Y : D
f : X ⟶ Y
this : f ≫ adj.unit.app Y = adj.unit.app X ≫ F.map (G.map f)
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) (adj.unit.app X ≫ F.map (G.map f)) ↔ IsIso (G.map f)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst✝ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
⊢ Sieve.ofArrows X f ∈ J S ↔
    Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))

Tactic:
by
  refine ⟨fun hf ↦ ⟨fun {U u} ↦ ?_⟩, fun hf ↦ ?_⟩
  · obtain ⟨u, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective u
    replace hf := J.pullback_stable u hf
    rwa [← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc u] at hf
  · rw [← Sieve.pullback_id (S := Sieve.ofArrows X f),
      ← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc (𝟙 S)]
    exact Presheaf.imageSieve_mem J (Cofan.IsColimit.desc hc (fun i ↦ shrinkYoneda.{w}.map (f i)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 S))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
clear_value f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C
this : F = Discrete.functor f
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
by
  classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance
  convert! isPullback_of_cofan_isVanKampen hc i.as j.as
  exact (if_neg (mt Discrete.ext hi.symm)).symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ Mono (c.ι.app i)

Tactic:
clear_value f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C
this : F = Discrete.functor f
⊢ Mono (c.ι.app i)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : projectiveDimension X < ↑n
this : ∀ (i : ℕ), projectiveDimension X < ↑i → HasProjectiveDimensionLT X i
⊢ HasProjectiveDimensionLT X n

Tactic:
exact this _ h

Goal state after: