mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
A : Type u
inst✝¹ : SmallCategory A
inst✝ : IsCardinalFiltered A κ
⊢ PreservesColimitsOfShape A (forget (CardinalDirectedPoset κ))

Tactic:
have := isFiltered_of_isCardinalFiltered A κ

Goal state after:
κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
A : Type u
inst✝¹ : SmallCategory A
inst✝ : IsCardinalFiltered A κ
this : IsFiltered A
⊢ PreservesColimitsOfShape A (forget (CardinalDirectedPoset κ))
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
A : Type u
inst✝¹ : SmallCategory A
inst✝ : IsCardinalFiltered A κ
this : IsFiltered A
⊢ PreservesColimitsOfShape A (ι ⋙ forget PartOrdEmb)

Tactic:
infer_instance

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝³ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
P : Set ↑J.obj → Prop
inst✝² : IsDirectedOrder (Subtype P)
inst✝¹ : Nonempty (Subtype P)
inst✝ : ∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ
S : Subtype P
⊢ PartOrdEmb.isCardinalFiltered κ { carrier := ↑↑S, str := Subtype.partialOrder fun x ↦ x ∈ ↑S }

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredGenerator C κ
P : ObjectProperty C
w✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤

Tactic:
exact hP.essentiallyLarge_top

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredColimits C κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
this✝ : W.isLocal.IsClosedUnderColimitsOfShape J
this : HasColimitsOfShape J C
⊢ PreservesColimitsOfShape J W.isLocal.ι

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} ((f : ↑W.toSet) × ((↑f).left ⟶ Z))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁴ : HasCoproduct D₁.obj₁
inst✝³ : HasCoproduct D₁.obj₂
inst✝² : HasPushouts C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} ((f : ↑W.toSet) × { pq // (↑f).hom ≫ pq.1 = (↑f).hom ≫ pq.2 })

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁴ : HasCoproduct D₁.obj₁
inst✝³ : HasCoproduct D₁.obj₂
inst✝² : HasPushouts C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₂ W Z)

Tactic:
infer_instance

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

Goal state before:
pp: X✝ X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
this : Fact κ.IsRegular
⊢ IsPresentable.{u, u, u + 1} X

Tactic:
have := hX.isCardinalPresentable

Goal state after:
X✝ X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
this✝ : Fact κ.IsRegular
this : IsCardinalPresentable X κ
⊢ IsPresentable.{u, u, u + 1} X
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W✝ : C
h : W✝ ⟶ Y
w✝ : EffectiveEpi h
i : W✝ ⟶ Z
this : i ≫ π = h ≫ f
W : C
g : W ⟶ Y
hg : Presieve.singleton h g
⊢ ∃ W_1 i e, S e ∧ i ≫ e = g ≫ f

Tactic:
cases hg

Goal state after:
case refine_2.mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ ∃ W_1 i e, S e ∧ i ≫ e = h ≫ f
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ X_1 f, (S = Presieve.ofArrows (fun x ↦ X_1) fun x ↦ f) ∧ EffectiveEpi f},
      ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
intro X Y f S ⟨Z, π, hπ, h_epi⟩
    have := Preregular.exists_fac f π
    obtain ⟨W, h, _, i, this⟩ := this
    refine ⟨Presieve.singleton h, ⟨?_, ?_⟩⟩
    · exact ⟨W, h, by {rw [Presieve.ofArrows_pUnit h]}, inferInstance⟩
    · intro W g hg
      cases hg
      refine ⟨Z, i, π, ⟨?_, this⟩⟩
      cases hπ
      rw [Presieve.ofArrows_pUnit]
      exact Presieve.singleton.mk

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 B : C
f : X ⟶ B
g : Y ⟶ B
inst✝¹ : HasPullback f g
inst✝ : IsRegularEpi f
⊢ IsRegularEpi f

Tactic:
infer_instance

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 B : C
f : X ⟶ B
g : Y ⟶ B
inst✝¹ : HasPullback f g
inst✝ : IsRegularEpi g
⊢ IsRegularEpi g

Tactic:
infer_instance

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

Goal state before:
pp: case refine_3
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j : J
hj : (D₂ D hι u).P j
⊢ ∀ (l₁ l₂ : j ⟶ m), (D₂ D hι u).W l₁ → (D₂ D hι u).W l₂ → l₁ = l₂

Tactic:
l₁

Goal state after:
case refine_3
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j : J
hj : (D₂ D hι u).P j
l₁ : j ⟶ m
⊢ ∀ (l₂ : j ⟶ m), (D₂ D hι u).W l₁ → (D₂ D hι u).W l₂ → l₁ = l₂
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
m : coequalizer (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
⊢ IsRegularEpi (pullback.fst k₂ e)

Tactic:
infer_instance

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

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

Tactic:
rintro j k f ((hf | ⟨⟨⟩⟩) | ⟨⟨i, j, hj⟩⟩)
        · simp only [Diagram.iSup_W, MorphismProperty.iSup_iff] at hf
          obtain ⟨i, hf⟩ := hf
          exact ⟨φ ⟨i, j, (D i).src hf⟩, φ ⟨i, k, (D i).tgt hf⟩, Or.inr ⟨_⟩, Or.inr ⟨_⟩,
            by simp [φ, (D i).isTerminal.comm_assoc _ hf]⟩
        · exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
        · refine ⟨φ ⟨i, j, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp [φ]⟩

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
⊢ IsRegularEpi (coequalizer.π (pullback.fst f f) (pullback.snd f f))

Tactic:
infer_instance

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
this : StrongEpi (imageFactorisation f A').F.e
⊢ IsRegularEpi (imageFactorisation f A').F.e

Tactic:
infer_instance

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
| coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
      ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) ≫
    colimMap
      (parallelPairHom (TensorBimod.actRight M (regular Y) ▷ N.X)
        ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) (M.actRight ▷ N.X)
        ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) (RightUnitorBimod.hom M ▷ Y.X ▷ N.X) (RightUnitorBimod.hom M ▷ N.X) ⋯
        ⋯)

Tactic:
rw [ι_colimMap, parallelPairHom_app_one]

Goal state after:
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
| RightUnitorBimod.hom M ▷ N.X ≫
    colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one
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:
infer_instance

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

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ (coherentCoverage C).coverings Y
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

Tactic:
obtain ⟨a, h, Y', π, h', _⟩ := hS
      refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
      obtain ⟨rfl, _⟩ := h'
      exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩

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

Goal state before:
pp: case refine_1
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₁ π₁
β : Type
w✝ : Finite β
Y₂ : β → D
τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂
H : EffectiveEpiFamily Y₂ τ₂
i : β → α
ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))
hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f
⊢ EffectiveEpiFamily (fun a ↦ F.obj ⋯.some.p) fun a ↦ F.effectiveEpiOver (Y₂ a) ≫ τ₂ a

Tactic:
infer_instance

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
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
x✝ : ofArrows w✝¹ w✝ f✝
g✝ : Z✝ ⟶ X
hg : ofArrows w✝¹ w✝ g✝
⊢ HasPullback f✝ g✝

Tactic:
cases hg

Goal state after:
case mk
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
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
Y✝ : C
f✝ : Y✝ ⟶ X
x✝ : ofArrows w✝¹ w✝ f✝
i✝ : w✝³
⊢ HasPullback f✝ (w✝ i✝)
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
this : Sigma.desc π' ≫ g = Sigma.desc π₂
⊢ EffectiveEpi (Sigma.desc π' ≫ g)

Tactic:
infer_instance

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

Goal state before:
pp: case refine_1
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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.EffectivelyEnough
inst✝² : Preregular D
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Z✝ ⟶ Y✝
x✝ : EffectiveEpi g
W : D
f' : W ⟶ F.obj X✝
w✝ : EffectiveEpi f'
i : W ⟶ F.obj Z✝
w : i ≫ F.map g = f' ≫ F.map f
⊢ EffectiveEpi (F.effectiveEpiOver W ≫ f')

Tactic:
infer_instance

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

Goal state before:
pp: case refine_2
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.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpi (F.effectiveEpiOver B)

Tactic:
infer_instance

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

Goal state before:
pp: case mp
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
⊢ IsLocallySurjective φ → Epi φ

Tactic:
intro

Goal state after:
case mp
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : IsLocallySurjective φ
⊢ Epi φ
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : IsLocallySurjective φ
⊢ Epi φ

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
⊢ Epi φ → IsLocallySurjective φ

Tactic:
intro

Goal state after:
case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
⊢ IsLocallySurjective φ
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝³ : IsLocallySurjective data.i
this✝² : IsLocallyInjective data.p
this✝¹ : Epi data.p
this✝ : Mono data.p
this : IsIso data.p
⊢ IsLocallySurjective (data.i ≫ data.p)

Tactic:
infer_instance

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

Goal state before:
pp: case refine_2.refine_1
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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ EffectiveEpi (g₀ ≫ π)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : PreservesFiniteProducts s
hF : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s)

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)

Tactic:
infer_instance

Goal state after: