mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ (∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'

Tactic:
constructor

Goal state after:
case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ ∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)

case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) ((ConcreteCategory.hom (f.app X)) m₁) =
    (ModuleCat.Hom.hom (g₂.app X)) ((ConcreteCategory.hom (f.app X)) m₁)

Tactic:
exact ConcreteCategory.congr_hom ((evaluation R X ⋙ forget _).congr_map hg) m₁

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)

Tactic:
let P : IsLimit c := limit.isLimit _

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.map f ≫ ↾fun x ↦ ModuleCat.freeMk x) = (↾fun x ↦ ModuleCat.freeMk x) ≫ ((freeObj F).presheaf ⋙ forget Ab).map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : F.obj X
⊢ (ConcreteCategory.hom (F.map f ≫ ↾fun x ↦ ModuleCat.freeMk x)).toFun x✝ =
    (ConcreteCategory.hom ((↾fun x ↦ ModuleCat.freeMk x) ≫ ((freeObj F).presheaf ⋙ forget Ab).map f)).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
⊢ (fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab))
      ((fun φ ↦ freeObjDesc φ) φ) =
    φ

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
x✝¹ : Cᵒᵖ
x✝ : F.obj x✝¹
⊢ (ConcreteCategory.hom
          (((fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab))
                ((fun φ ↦ freeObjDesc φ) φ)).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (φ.app x✝¹)).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G✝ : PresheafOfModules R
F₁ F₂ : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
f : F₁ ⟶ F₂
g : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G
⊢ freeAdjunctionUnit R F₁ ≫ Functor.whiskerRight ((toPresheaf R).map (freeHomEquiv.symm (f ≫ g))) (forget Ab) =
    freeAdjunctionUnit R F₁ ≫
      Functor.whiskerRight ((toPresheaf R).map ((free R).map f ≫ freeHomEquiv.symm g)) (forget Ab)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G✝ : PresheafOfModules R
F₁ F₂ : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
f : F₁ ⟶ F₂
g : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G
x✝¹ : Cᵒᵖ
x✝ : F₁.obj x✝¹
⊢ (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map (freeHomEquiv.symm (f ≫ g))) (forget Ab)).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map ((free R).map f ≫ freeHomEquiv.symm g)) (forget Ab)).app
            x✝¹)).toFun
      x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ RingCat.Hom.hom (cR.ι.app X) = (RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))

Tactic:
ext

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = ((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
T : Eᵒᵖ ⥤ RingCat
G : D ⥤ E
ψ : R ⟶ G.op ⋙ T
T' : E'ᵒᵖ ⥤ RingCat
G' : E ⥤ E'
ψ' : T ⟶ G'.op ⋙ T'
⊢ (pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (φ ≫ F.op.whiskerLeft ψ) ψ' =
    ((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫ pushforwardComp φ (ψ ≫ G.op.whiskerLeft ψ')

Tactic:
ext

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
T : Eᵒᵖ ⥤ RingCat
G : D ⥤ E
ψ : R ⟶ G.op ⋙ T
T' : E'ᵒᵖ ⥤ RingCat
G' : E ⥤ E'
ψ' : T ⟶ G'.op ⋙ T'
x✝¹ : PresheafOfModules T'
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom
        ((((pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (φ ≫ F.op.whiskerLeft ψ) ψ').hom.app
              x✝¹).app
          X✝))
      x✝ =
    (ModuleCat.Hom.hom
        (((((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
                    isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
                      pushforwardComp φ (ψ ≫ G.op.whiskerLeft ψ')).hom.app
              x✝¹).app
          X✝))
      x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
⊢ pushforwardComp (𝟙 S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
x✝¹ : PresheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp (𝟙 S) φ).hom.app x✝¹).app X✝)) x✝ =
    (ModuleCat.Hom.hom
        ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x✝¹).app X✝))
      x✝
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
⊢ homOfLe h ≫ G'.ι = G.ι

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
x✝¹ : C
x✝ : G.toFunctor.obj x✝¹
⊢ (hom ((homOfLe h ≫ G'.ι).app x✝¹)).toFun x✝ = (hom (G.ι.app x✝¹)).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
⊢ pushforwardComp φ (𝟙 R) = isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
x✝¹ : PresheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp φ (𝟙 R)).hom.app x✝¹).app X✝)) x✝ =
    (ModuleCat.Hom.hom
        (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x✝¹).app X✝))
      x✝
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ G = ⊤ ↔ IsIso G.ι

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ G = ⊤ → IsIso G.ι

case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ IsIso G.ι → G = ⊤
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPretopology

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J → K ≤ J.toPretopology

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K ≤ J.toPretopology → K.toGrothendieck ≤ J
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯ = 𝟙 (Limits.pullback g f)

Tactic:
ext

Goal state after:
case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.fst g f = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)} →
      Sieve.pullback f S ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
by
    intro X Y S h H Z f
    rcases H (f ≫ h) with ⟨W, g, H'⟩
    exact ⟨W, g, by simpa⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ (Presieve.singleton g).bind Ti K ↔ Presieve.singleton (f ≫ g) K

Tactic:
constructor

Goal state after:
case refine_2.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ (Presieve.singleton g).bind Ti K → Presieve.singleton (f ≫ g) K

case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ Presieve.singleton (f ≫ g) K → (Presieve.singleton g).bind Ti K
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
inst✝¹ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst✝ : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ Presieve.pullbackArrows f (Presieve.ofArrows Z g) ∈ J.coverings X

Tactic:
rw [← Presieve.ofArrows_pullback]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
inst✝¹ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst✝ : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ (Presieve.ofArrows (fun i ↦ Limits.pullback (g i) f) fun x ↦ Limits.pullback.snd (g x) f) ∈ J.coverings X
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
⊢ comap (𝟭 C) K = K

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
x✝¹ : C
x✝ : Presieve x✝¹
⊢ x✝ ∈ (comap (𝟭 C) K).coverings x✝¹ ↔ x✝ ∈ K.coverings x✝¹
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y✝ : C
i : ι
Y : C
j : κ (g i) ⋯
⊢ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) (fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) (p (g i) ⋯ j ≫ g i)

Tactic:
exact .mk <| Sigma.mk (β := fun i : ι ↦ κ (g i) ⟨i⟩) i j

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P → ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) → IsSheaf K.toGrothendieck P
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
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
⊢ y' ≫ g = y' ≫ h

Tactic:
ext

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
x✝ : PUnit.{u + 1}
⊢ (hom (y' ≫ g)).toFun x✝ = (hom (y' ≫ h)).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g ↔ f = g

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g → f = g

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h ↔ singleton (pullback.snd g f) h

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h → singleton (pullback.snd g f) h

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ singleton (pullback.snd g f) h → pullbackArrows f (singleton g) h
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
⊢ ofArrows Y f (f i)

Tactic:
constructor

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h ↔ pullbackArrows f (ofArrows Z g) h

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h → pullbackArrows f (ofArrows Z g) h

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ pullbackArrows f (ofArrows Z g) h → ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (ofArrows Z g).bind (fun x f H ↦ ofArrows (W f H) (k f H)) f ↔
    ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) (fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) f

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (ofArrows Z g).bind (fun x f H ↦ ofArrows (W f H) (k f H)) f →
    ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) (fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) f

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) (fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) f →
    (ofArrows Z g).bind (fun x f H ↦ ofArrows (W f H) (k f H)) f
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) ↔ Nonempty (IsColimit S.arrows.cocone)

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit S.arrows.cocone)

case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := ⋯
⊢ (fun t ↦ x.IsAmalgamation t) (H.desc s) ∧
    ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = H.desc s

Tactic:
constructor

Goal state after:
case h.left
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := ⋯
⊢ (fun t ↦ x.IsAmalgamation t) (H.desc s)

case h.right
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := ⋯
⊢ ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = H.desc s
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 : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ functorPushforward (F ⋙ G) R f ↔ functorPushforward G (functorPushforward F R) f

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ functorPushforward (F ⋙ G) R f → functorPushforward G (functorPushforward F R) f

case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ functorPushforward G (functorPushforward F R) f → functorPushforward (F ⋙ G) R f
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 : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ map F (ofArrows Y f) = ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)

Tactic:
by
  refine le_antisymm (fun Z g hg ↦ ?_) fun _ _ ⟨i⟩ ↦ map_map ⟨i⟩
  obtain ⟨hu⟩ := hg
  obtain ⟨i, rfl, rfl⟩ := Presieve.ofArrows_surj _ _ hu
  simpa using ofArrows.mk i

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry ↔ ⟨Z, v⟩ ∈ {⟨Y, u⟩}

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry → ⟨Z, v⟩ ∈ {⟨Y, u⟩}

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ {⟨Y, u⟩} → ⟨Z, v⟩ ∈ (singleton u).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton ⟨Z, v⟩.snd).uncurry

Tactic:
constructor

Goal state after: