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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
V W X Y Z : Mon C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ whiskerRight (M.associatorBimod N P).hom Q ≫
      (M.associatorBimod (N.tensorBimod P) Q).hom ≫ M.whiskerLeft (N.associatorBimod P Q).hom =
    ((M.tensorBimod N).associatorBimod P Q).hom ≫ (M.associatorBimod N (P.tensorBimod Q)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
⊢ f₁ ≫ t ≫ IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t) = f₂ ≫ t ≫ IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f✝ : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject A
B' : Subobject B
⊢ IsRegularEpi (frobeniusMorphism f A' B')

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f✝ : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject A
B' : Subobject B
⊢ frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').arrow = (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
inst✝ : CartesianMonoidalCategory A
X Y : Sheaf J A
⊢ Presheaf.IsSheaf J (X.obj ⊗ Y.obj)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
inst✝ : CartesianMonoidalCategory A
⊢ Presheaf.IsSheaf J (𝟙_ (Cᵒᵖ ⥤ A))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
j : J
hj : D.P j
f : j ⟶ m₁
hf : (D₄ D φ).W f
⊢ f = φ ⟨j, hj⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)

Tactic:
rw [← Sieve.generateFamily_eq] at h_colim

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
W : C
⊢ Presieve.IsSheaf (coherentTopology C) (yoneda.obj W)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ ((adjunction J adj).unit.app X).hom =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj ≫ whiskerRight (toSheafify J (X.obj ⋙ G)) F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
Y : Sheaf J D
⊢ (sheafToPresheaf J D).map
      ((Iso.refl (sheafToPresheaf J E ⋙ (whiskeringRight Cᵒᵖ E D).obj G ⋙ presheafToSheaf J D)).inv.app
          ((sheafCompose J F).obj Y) ≫
        ((whiskeringRight Cᵒᵖ E D).obj G ⋙ presheafToSheaf J D).map
            ((Iso.refl (𝟭 (Sheaf J D) ⋙ sheafToPresheaf J D ⋙ (whiskeringRight Cᵒᵖ D E).obj F)).inv.app Y) ≫
          ((Adjunction.whiskerRight Cᵒᵖ adj).comp (sheafificationAdjunction J D)).counit.app ((𝟭 (Sheaf J D)).obj Y)) =
    sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
f : m₁ ⟶ m₁
hf : (D₄ D φ).W f
⊢ f = 𝟙 m₁

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ E D).obj G) f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁵ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝⁴ : HasWeakSheafify J D
FD : D → D → Type u_2
CD : D → Type (max u₁ v₁)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : (forget D).IsRightAdjoint
⊢ (sheafForget J).IsRightAdjoint

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
⊢ ∀ ⦃j : J⦄, (D₄ D φ).P j → ∃ lift, (D₄ D φ).W lift

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : Presieve.ofArrows Y π x✝
⊢ S.arrows x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ (coherentTopology C) X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x ↦
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x ↦
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ (Presieve.ofArrows (fun c ↦ Y_n c.fst c.snd) fun c ↦ π_n c.fst c.snd ≫ π c.fst).EffectiveEpimorphic

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
⊢ ∀ ⦃j : J⦄, (D₄ D φ).P j → ∀ (l₁ l₂ : j ⟶ m₁), (D₄ D φ).W l₁ → (D₄ D φ).W l₂ → l₁ = l₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ 𝟙 (Y_n i b) ≫ π_n i b ≫ π i = π_n i b ≫ π i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpiFamily (fun c ↦ Y_n c.fst c.snd) fun c ↦ π_n c.fst c.snd ≫ π c.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y Z : α → C
π : (a : α) → Y a ⟶ X
inst✝ : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpi (f a)
⊢ EffectiveEpiFamily Z fun a ↦ f a ≫ π a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ 𝟙 Y' a' ≫ π a' = π a'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ ∀ (a : Unit), ⊤.arrows ((fun x ↦ 𝟙 Y) a)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ (M.associatorBimod (regular Y) N).hom ≫ M.whiskerLeft N.leftUnitorBimod.hom = whiskerRight M.rightUnitorBimod.hom N

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ (coherentTopology C) X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
X Y : J
i✝ : Unit
⊢ 𝟙 m₁ ≫ 𝟙 m₁ = 𝟙 m₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
X Y j : J
hj : D.P j
⊢ φ ⟨j, hj⟩ ≫ 𝟙 m₁ = φ ⟨j, hj⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
⊢ ∀ ⦃i j : J⦄ (f : i ⟶ j), (D₄ D φ).W f → ∃ li lj, (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ f ≫ lj = li

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ ⟨j, hj⟩
j : J
hj : (D₄ D φ).IsTerminal j
⊢ j = m₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ ⟨j, hj⟩
D₄' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₄ D φ;
  { toDiagram := __Diagram, top := m₁, isTerminal := hm₁, uniq_terminal := ⋯ }
⊢ f₁ ≫ (functor J κ).map (homOfLE ⋯) = f₂ ≫ (functor J κ).map (homOfLE ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
⊢ (functor J κ).Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
this : IsFiltered κ.ord.ToType
x✝¹ : J × κ.ord.ToType
j : J
x : κ.ord.ToType
x✝ : (j, Order.succ x) ⟶ (j, x)
fst✝ : (j, Order.succ x).1 ⟶ (j, x).1
f : (j, Order.succ x).2 ⟶ (j, x).2
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ ∃ α x, ∃ (_ : IsCardinalFiltered α κ), ∃ F, F.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w✝¹ : PartialOrder α
w✝ : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h✝ : F.Final
⊢ IsFiltered α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent

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
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
⊢ ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ∃ α x, ∃ (_ : IsDirected α fun x1 x2 ↦ x1 ≤ x2) (_ : Nonempty α), ∃ F, F.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S
⊢ S ∈ (regularTopology C) X

Tactic:
apply Coverage.saturate_of_superset (regularCoverage C) h_le

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S
⊢ (regularCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ (∃ Y π, EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C) X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
h₂ : Sieve.generate (Presieve.ofArrows ?m.50 ?m.51) ∈ (regularTopology C) X
⊢ (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π).EffectiveEpimorphic

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
X : C
S : Presieve X
inst✝ : S.Extensive
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
X : C
S : Presieve X
inst✝¹ : S.Extensive
F : Cᵒᵖ ⥤ Type w
inst✝ : PreservesFiniteProducts F
⊢ IsSheafFor F S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W : C
⊢ IsSheaf (extensiveTopology C) (yoneda.obj W)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
inst✝ : HasFiniteCoproducts C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
x✝ : EffectiveEpi g
⊢ ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
V : C
f : V ⟶ X
i✝ : Unit
h : V ⟶ Y
hf : h ≫ π = f
⊢ 𝟙 Y' ≫ π' ≫ π = π' ≫ π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ EffectiveEpi (π' ≫ π)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y Y' : C
π : Y' ⟶ Y
right✝ : EffectiveEpi π
⊢ 𝟙 Y' ≫ π = π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
⊢ ⊤.arrows (𝟙 Y)

Tactic:
by

Goal state after: