mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
inst✝⁶ : MonoidalCategory D✝
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : MonoidalCategory D
inst✝¹ : MonoidalCategory E
L : D ⥤ E
inst✝ : L.OplaxMonoidal
⊢ ∀ (X : C ⥤ D),
    (λ_ (((Functor.whiskeringRight C D E).obj L).obj X)).inv =
      ((Functor.whiskeringRight C D E).obj L).map (λ_ X).inv ≫
        { app := fun X_1 ↦ δ L ((𝟙_ (C ⥤ D)).obj X_1) (X.obj X_1), naturality := ⋯ } ≫
          { app := fun X ↦ η L, naturality := ⋯ } ▷ ((Functor.whiskeringRight C D E).obj L).obj X

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
inst✝⁶ : MonoidalCategory D✝
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : MonoidalCategory D
inst✝¹ : MonoidalCategory E
L : D ⥤ E
inst✝ : L.OplaxMonoidal
⊢ ∀ (X : C ⥤ D),
    (ρ_ (((Functor.whiskeringRight C D E).obj L).obj X)).inv =
      ((Functor.whiskeringRight C D E).obj L).map (ρ_ X).inv ≫
        { app := fun X_1 ↦ δ L (X.obj X_1) ((𝟙_ (C ⥤ D)).obj X_1), naturality := ⋯ } ≫
          ((Functor.whiskeringRight C D E).obj L).obj X ◁ { app := fun X ↦ η L, naturality := ⋯ }

Tactic:
aesop

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

Goal state before:
pp: case symm
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ y✝ : (j : C) × F.obj j
a✝ : Relation.EqvGen F.ColimitTypeRel x✝ y✝
ih : Zigzag x✝.fst y✝.fst
⊢ Zigzag y✝.fst x✝.fst

Tactic:
| symm _ _ _ ih =>

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFiltered C
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
⊢ (map f).Final

Tactic:
have := NatIso.isIso_of_isIso_app (𝟙 T)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFiltered C
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
this : IsIso (𝟙 T)
⊢ (map f).Final
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)
P : IsLimit c := limit.isLimit (uncurry.obj F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun j ↦ limit.isLimit (F.obj j)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)

Tactic:
have Q' := coneOfConeUncurryIsLimit Q P

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)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun j ↦ limit.isLimit (F.obj j)
Q' : IsLimit (coneOfConeUncurry Q c)
⊢ 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
⊢ ∀ (X : Cᵒᵖ),
    ModuleCat.freeDesc (↾fun x ↦ ModuleCat.freeMk ((ConcreteCategory.hom (F.map (𝟙 X))) x)) =
      (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app
        ((ModuleCat.free ↑(R.obj X)).obj (F.obj X))

Tactic:
aesop

Goal state after:
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 : D ⥤ C
X : F.PartialLeftAdjointSource
Y Y' : D
f : F.partialLeftAdjointObj X ⟶ Y
g : Y ⟶ Y'
⊢ F.partialLeftAdjointHomEquiv (f ≫ g) = F.partialLeftAdjointHomEquiv f ≫ F.map g

Tactic:
apply CorepresentableBy.homEquiv_comp

Goal state after:
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 : D ⥤ C
h : ∀ (X : C), (F ⋙ coyoneda.obj (op X)).IsCorepresentable
X : C
Y Y' : D
g : Y ⟶ Y'
f : (F ⋙ coyoneda.obj (op X)).coreprX ⟶ Y
⊢ (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv (f ≫ g) =
    (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv f ≫ F.map g

Tactic:
apply CorepresentableBy.homEquiv_comp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ (F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃).hom =
    ((F₀₁.associator F₁₂ F₂₃).symm ≪≫
        isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫
          adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃).hom

Tactic:
exact leftAdjointCompNatTrans_assoc _ _ _ _ _ _ _ _ _ _
    (by simpa using congr_arg Iso.inv h)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝⁴ : Set (Subfunctor F)
x✝³ : Subfunctor F
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : F.obj x✝¹
⊢ x✝ ∈ x✝³.obj x✝¹ → x✝ ∈ { obj := fun U ↦ sSup ((fun T ↦ T.obj U) '' x✝⁴), map := ⋯ }.obj x✝¹

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝³ : Set (Subfunctor F)
x✝² : Subfunctor F
x✝¹ : x✝² ∈ upperBounds x✝³
x✝ : C
⊢ { obj := fun U ↦ sSup ((fun T ↦ T.obj U) '' x✝³), map := ⋯ }.obj x✝ ⊆ x✝².obj x✝

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝⁴ : Set (Subfunctor F)
x✝³ : Subfunctor F
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : F.obj x✝¹
⊢ x✝ ∈ { obj := fun U ↦ sInf ((fun T ↦ T.obj U) '' x✝⁴), map := ⋯ }.obj x✝¹ → x✝ ∈ x✝³.obj x✝¹

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝³ : Set (Subfunctor F)
x✝² : Subfunctor F
x✝¹ : x✝² ∈ lowerBounds x✝³
x✝ : C
⊢ x✝².obj x✝ ⊆ { obj := fun U ↦ sInf ((fun T ↦ T.obj U) '' x✝³), map := ⋯ }.obj x✝

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
S₁ S₂ T : Subfunctor F
⊢ (S₁ ⊔ S₂) ⊓ T = S₁ ⊓ T ⊔ S₂ ⊓ T

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
ι : Sort u_1
S : ι → Subfunctor F
T : Subfunctor F
⊢ (⨆ i, S i) ⊓ T = ⨆ i, S i ⊓ T

Tactic:
aesop

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

Goal state before:
pp: 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}
⊢ (Presieve.singleton g).bind Ti ∈ {S | ∃ Y f, ∃ (_ : IsIso f), S = Presieve.singleton f}

Tactic:
rcases hS g (singleton_self g) with ⟨Y, f, i, hTi⟩

Goal state after:
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
⊢ (Presieve.singleton g).bind Ti ∈ {S | ∃ Y f, ∃ (_ : IsIso f), S = Presieve.singleton 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 Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝³.arrows f → x✝¹.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝².arrows f → x✝¹.arrows f
x✝ : C
f : x✝ ⟶ X
⊢ (x✝³.union x✝²).arrows f → x✝¹.arrows f

Tactic:
rintro (hf | hf)
    · exact h₁ _ hf
    · exact h₂ _ hf

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
⊢ S.arrows (i ≫ f) ↔ S.arrows f

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
  convert! S.downward_closed H (inv i)
  simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop X)) j✝ ≫
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramNatTrans η (unop Y)) =
    colimit.ι (J.diagram P (unop X)) j✝ ≫
      colimMap (J.diagramNatTrans η (unop X)) ≫
        colimMap (J.diagramPullback Q f.unop) ≫ colimit.pre (J.diagram Q (unop Y)) (J.pullback f.unop).op

Tactic:
simp only [diagramPullback_app, ι_colimMap, colimit.ι_pre_assoc, colimit.ι_pre,
      ι_colimMap_assoc, Category.assoc]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
⊢ Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index P) ((J.diagram P (unop X)).obj j✝)
        (fun I ↦ Multiequalizer.ι ((unop j✝).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagramNatTrans η (unop Y)).app ((J.pullback f.unop).op.obj j✝) ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝) =
    (J.diagramNatTrans η (unop X)).app j✝ ≫
      Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index Q) ((J.diagram Q (unop X)).obj j✝)
          (fun I ↦ Multiequalizer.ι ((unop j✝).index Q) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝)
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
⊢ range (𝟙 F) = ⊤

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

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

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((toRange p).app i))

Tactic:
rw [← epi_iff_surjective]

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Epi ((toRange p).app i)
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
f : F ⟶ F'
g : F' ⟶ F''
x✝² : C
x✝¹ : F''.obj x✝²
x✝ : x✝¹ ∈ (range (f ≫ g)).obj x✝²
⊢ x✝¹ ∈ (range g).obj x✝²

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
f : F ⟶ F'
⊢ ⊤.image f = range f

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
ι : Type u_1
G : ι → Subfunctor F
f : F ⟶ F'
⊢ (⨆ i, G i).image f = ⨆ i, (G i).image f

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
f : F ⟶ F'
g : F' ⟶ F''
⊢ G.image (f ≫ g) = (G.image f).image g

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
f : F ⟶ F'
g : F' ⟶ F''
⊢ range (f ≫ g) = (range f).image g

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ G.preimage (𝟙 F) = G

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
f : F'' ⟶ F'
g : F' ⟶ F
⊢ G.preimage (f ≫ g) = (G.preimage g).preimage f

Tactic:
aesop

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

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
X : A'ᵒᵖ
q : Presieve.IsSheafFor (P' ⋙ coyoneda.obj X) (generate R).arrows
⊢ IsLimit ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P') ⋯))

Tactic:
← Presieve.isSheafFor_iff_generate

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
X : A'ᵒᵖ
q : Presieve.IsSheafFor (P' ⋙ coyoneda.obj X) R
⊢ IsLimit ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P') ⋯))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      (ConcreteCategory.hom (P.map f.op)) t₁ = b → (ConcreteCategory.hom (P.map f.op)) t₂ = b → t₁ = t₂) ↔
    ∀ ⦃a₁ a₂ : P.obj (op Y)⦄, (ConcreteCategory.hom (P.map f.op)) a₁ = (ConcreteCategory.hom (P.map f.op)) a₂ → a₁ = a₂

Tactic:
aesop

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

Goal state before:
pp: 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, s.IsAmalgamation t

Tactic:
let t : Presieve.FamilyOfElements P (U : Presieve X) :=
    fun Y f hf => (hB hf).amalgamate (y hf) (hy hf)

Goal state after:
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) ⋯
⊢ ∃! t, s.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
⊢ Presieve.IsSheaf J G.toFunctor ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U

Tactic:
by
  rw [← G.eq_sheafify_iff h]
  change _ ↔ G.sheafify J ≤ G
  exact ⟨Eq.ge, (G.le_sheafify J).antisymm⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom

Tactic:
apply Subfunctor.sheafify_le

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom

case hF
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presieve.IsSheaf J F'.obj

case hG'
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presieve.IsSheaf J (Subfunctor.range I.m.hom).toFunctor
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
x : { p // f p.1 = g p.2 }
⊢ (fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩) ((fun x ↦ ⟨(↑x).1, ⋯⟩) x) = x

Tactic:
ext <;> dsimp

Goal state after:
case snd
J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
x : { p // f p.1 = g p.2 }
⊢ Exists.choose ⋯ = (↑x).2
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (range ⇑(ConcreteCategory.hom c.inl))ᶜ

Tactic:
· change IsOpen (Set.range c.inl)ᶜ
            rw [← eq_compl_iff_isCompl.mpr h₃.symm]
            exact h₂.isOpen_range

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

Tactic:
rw [← Function.Bijective.of_comp_iff _ (Iso.homToEquiv e).bijective]

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
⊢ Function.Bijective ((fun g ↦ f ≫ g) ∘ ⇑e.homToEquiv)
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
⊢ (fun g ↦ f ≫ g) ∘ ⇑e.homToEquiv = ⇑e.homToEquiv ∘ fun g ↦ f ≫ g

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
X X' : C
e : X ≅ X'
hX : W.isColocal X
Y Z : C
g : Y ⟶ Z
hg : W g
⊢ (fun f ↦ f ≫ g) ∘ ⇑e.homFromEquiv = ⇑e.homFromEquiv ∘ fun f ↦ f ≫ g

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
h : W ≤ W'
f : C
hf : W'.isLocal f
⊢ W.isLocal f

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
h : W ≤ W'
f : C
hf : W'.isColocal f
⊢ W.isColocal f

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_1
W : ι → MorphismProperty C
⊢ (⨆ i, W i).isLocal = ⨅ i, (W i).isLocal

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_1
W : ι → MorphismProperty C
⊢ (⨆ i, W i).isColocal = ⨅ i, (W i).isColocal

Tactic:
aesop

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
let : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') :=
    Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso.symm

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso := (CatCommSq.iso (F ⋙ G) L₂ L₂ (F' ⋙ G')).symm }
⊢ (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case e'_3
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
Y : C
e_1✝ : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)
e_2✝ : ((𝟭 D).obj X ⟶ F.obj Y) = (X ⟶ F.obj Y)
⊢ (fun g ↦ adj.unit.app X ≫ g) =
    (fun f ↦ adj.unit.app X ≫ F.map f) ∘ ⇑(Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm

Tactic:
aesop

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve X
hS : S ∈ J X
Z : Cᵒᵖ ⥤ Type w
hZ : Presieve.IsSheaf J Z
⊢ Presieve.IsSheafFor Z S.arrows

Tactic:
exact hZ _ hS

Goal state after: