awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
mp : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
mp₁ : (c.fst ≫ φ) ≫ c.snd = 𝟙 c.pt ≫ c.snd
⊢ IsIso c.fst

Tactic:
refine ⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst

Tactic:
simp only [assoc, hφ₁, id_comp, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ (c.fst ≫ φ) ≫ c.snd = 𝟙 c.pt ≫ c.snd

Tactic:
simp only [assoc, hφ₂, id_comp, comp_id, h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
mpr : ∀ (φ : X ⟶ c.pt) (hφ₁ : φ ≫ c.fst = 𝟙 X) (hφ₂ : φ ≫ c.snd = 𝟙 X), c.fst = c.snd
⊢ c.fst = c.snd

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.PullbackCone.IsLimit.lift'
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
rw : (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst
rw₁ : c.fst ≫ φ ≫ c.fst = 𝟙 c.pt ≫ c.fst
rw₂ : c.fst ≫ φ ≫ c.fst = c.fst
rw₃ : c.fst ≫ 𝟙 X = c.fst
rw₄ rw₅ : c.fst = c.fst
⊢ c.fst ≫ φ = 𝟙 c.pt

Tactic:
rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ IsSplitEpi φ

Tactic:
have : IsSplitEpi φ := IsSplitEpi.mk ⟨SplitEpi.mk c.fst (by
      rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id])⟩
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
this : IsSplitEpi φ
mpr : φ ≫ c.fst = φ ≫ c.snd
mpr₁ : 𝟙 X = φ ≫ c.snd
mpr₂ mpr₃ : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) (𝟙 X)
⊢ c.fst = c.snd

Tactic:
rw [← cancel_epi φ, hφ₁, hφ₂]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Mono f ↔ IsIso c.snd

Tactic:
mono_iff_isIso_fst (PullbackCone.flipIsLimit hc)

Premises used: CategoryTheory.Limits.PullbackCone.flipIsLimit, CategoryTheory.mono_iff_isIso_fst
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
mp : Mono f → IsPullback (𝟙 X) (𝟙 X) f f
mpr : IsPullback (𝟙 X) (𝟙 X) f f → Mono f
⊢ Mono f ↔ IsPullback (𝟙 X) (𝟙 X) f f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : Mono f
⊢ IsPullback (𝟙 X) (𝟙 X) f f

Tactic:
IsPullback.of_isLimit (PullbackCone.isLimitMkIdId f)

Premises used: CategoryTheory.Limits.PullbackCone.isLimitMkIdId, CategoryTheory.IsPullback.of_isLimit
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : Mono f
⊢ IsPullback (𝟙 X) (𝟙 X) f f

Tactic:
exact IsPullback.of_isLimit (PullbackCone.isLimitMkIdId f)

Premises used: CategoryTheory.Limits.PullbackCone.isLimitMkIdId, CategoryTheory.IsPullback.of_isLimit
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPullback (𝟙 X) (𝟙 X) f f
⊢ Mono f

Tactic:
(mono_iff_fst_eq_snd hf.isLimit).2 rfl

Premises used: Iff.mpr, CategoryTheory.mono_iff_fst_eq_snd, rfl, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPullback (𝟙 X) (𝟙 X) f f
⊢ Mono f

Tactic:
exact (mono_iff_fst_eq_snd hf.isLimit).2 rfl

Premises used: Iff.mpr, CategoryTheory.mono_iff_fst_eq_snd, rfl, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
mp : Epi f → c.inl = c.inr
mpr : c.inl = c.inr → Epi f
⊢ Epi f ↔ c.inl = c.inr

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : Epi f
⊢ c.inl = c.inr

Tactic:
simpa only [← cancel_epi f] using c.condition

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
mpr : ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
⊢ Epi f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
h : f ≫ g = f ≫ g'
mpr : ∀ (φ : c.pt ⟶ Z) (h : f ≫ c.inl ≫ φ = f ≫ c.inr ≫ φ), c.inl ≫ φ = c.inr ≫ φ
⊢ g = g'

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.desc', rfl
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
φ : c.pt ⟶ Z
h : f ≫ c.inl ≫ φ = f ≫ c.inr ≫ φ
mpr mpr₁ : c.inr ≫ φ = c.inr ≫ φ
⊢ c.inl ≫ φ = c.inr ≫ φ

Tactic:
rw [hf]
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
rw : c.inl = c.inr ↔ IsIso c.inl
⊢ Epi f ↔ IsIso c.inl

Tactic:
rw [epi_iff_inl_eq_inr hc]

Premises used: CategoryTheory.epi_iff_inl_eq_inr
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
mp : c.inl = c.inr → IsIso c.inl
mpr : IsIso c.inl → c.inl = c.inr
⊢ c.inl = c.inr ↔ IsIso c.inl

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
mp : ∀ (φ : c.pt ⟶ Y) (hφ₁ : c.inl ≫ φ = 𝟙 Y) (hφ₂ : c.inr ≫ φ = 𝟙 Y), IsIso c.inl
⊢ IsIso c.inl

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.PushoutCocone.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ IsIso c.inl

Tactic:
⟨φ, hφ₁, PushoutCocone.IsColimit.hom_ext hc ?_ ?_⟩

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
mp : c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
mp₁ : c.inr ≫ φ ≫ c.inl = c.inr ≫ 𝟙 c.pt
⊢ IsIso c.inl

Tactic:
refine ⟨φ, hφ₁, PushoutCocone.IsColimit.hom_ext hc ?_ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt

Tactic:
simp only [comp_id, reassoc_of% hφ₁]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inr ≫ φ ≫ c.inl = c.inr ≫ 𝟙 c.pt

Tactic:
simp only [comp_id, h, reassoc_of% hφ₂]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
mpr : ∀ (φ : c.pt ⟶ Y) (hφ₁ : c.inl ≫ φ = 𝟙 Y) (hφ₂ : c.inr ≫ φ = 𝟙 Y), c.inl = c.inr
⊢ c.inl = c.inr

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.PushoutCocone.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
rw : c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
rw₁ : c.inl = c.inl ≫ 𝟙 c.pt
rw₂ rw₃ : c.inl = c.inl
⊢ φ ≫ c.inl = 𝟙 c.pt

Tactic:
rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id]

Premises used: CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Category.comp_id, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ IsSplitMono φ

Tactic:
have : IsSplitMono φ := IsSplitMono.mk ⟨SplitMono.mk c.inl (by
      rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id])⟩
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
this : IsSplitMono φ
mpr : c.inl ≫ φ = c.inr ≫ φ
mpr₁ : 𝟙 Y = c.inr ≫ φ
mpr₂ mpr₃ : Eq.{v_1 + 1} (α := Y ⟶ Y) (𝟙 Y) (𝟙 Y)
⊢ c.inl = c.inr

Tactic:
rw [← cancel_mono φ, hφ₁, hφ₂]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f ↔ IsIso c.inr

Tactic:
epi_iff_isIso_inl (PushoutCocone.flipIsColimit hc)

Premises used: CategoryTheory.Limits.PushoutCocone.flipIsColimit, CategoryTheory.epi_iff_isIso_inl
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
mp : Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)
mpr : IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f
⊢ Epi f ↔ IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : Epi f
⊢ IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
IsPushout.of_isColimit (PushoutCocone.isColimitMkIdId f)

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitMkIdId, CategoryTheory.IsPushout.of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : Epi f
⊢ IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
exact IsPushout.of_isColimit (PushoutCocone.isColimitMkIdId f)

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitMkIdId, CategoryTheory.IsPushout.of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPushout f f (𝟙 Y) (𝟙 Y)
⊢ Epi f

Tactic:
(epi_iff_inl_eq_inr hf.isColimit).2 rfl

Premises used: Iff.mpr, CategoryTheory.epi_iff_inl_eq_inr, CategoryTheory.IsPushout.isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPushout f f (𝟙 Y) (𝟙 Y)
⊢ Epi f

Tactic:
exact (epi_iff_inl_eq_inr hf.isColimit).2 rfl

Premises used: Iff.mpr, CategoryTheory.epi_iff_inl_eq_inr, CategoryTheory.IsPushout.isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.EssentiallySmall
Goal:
J : Type u₂
inst : Category.{v₂, u₂} J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : EssentiallySmall.{w₁, v₂, u₂} J
inst_3 : HasLimitsOfSize.{w₁, w₁, v₁, u₁} C
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
hasLimitsOfShape_of_equivalence <| Equivalence.symm <| equivSmallModel.{w₁} J

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Limits.EssentiallySmall
Goal:
J : Type u₂
inst : Category.{v₂, u₂} J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : EssentiallySmall.{w₁, v₂, u₂} J
inst_3 : HasColimitsOfSize.{w₁, w₁, v₁, u₁} C
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
hasColimitsOfShape_of_equivalence <| Equivalence.symm <| equivSmallModel.{w₁} J

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Limits.EssentiallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type w₂
inst_1 : Small.{w₁, w₂} β
inst_2 : HasProducts.{w₁, v₁, u₁} C
⊢ HasProductsOfShape.{w₂, u₁, v₁} β C

Tactic:
hasLimitsOfShape_of_equivalence <| Discrete.equivalence <| Equiv.symm <| equivShrink β

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, Equiv.symm, equivShrink
-- Module: Mathlib.CategoryTheory.Limits.EssentiallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type w₂
inst_1 : Small.{w₁, w₂} β
inst_2 : HasCoproducts.{w₁, v₁, u₁} C
⊢ HasCoproductsOfShape.{w₂, u₁, v₁} β C

Tactic:
hasColimitsOfShape_of_equivalence <| Discrete.equivalence <| Equiv.symm <| equivShrink β

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, Equiv.symm, equivShrink
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ leftExactFunctor C D F ↔ PreservesFiniteLimits F

Tactic:
Iff.rfl

Premises used: CategoryTheory.leftExactFunctor, Iff.rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : leftExactFunctor C D X
⊢ PreservesFiniteLimits X

Tactic:
simp only [leftExactFunctor_iff] at h ⊢

Premises used: CategoryTheory.leftExactFunctor_iff
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : PreservesFiniteLimits X
⊢ PreservesFiniteLimits Y

Tactic:
preservesFiniteLimits_of_natIso e

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : PreservesFiniteLimits X
⊢ PreservesFiniteLimits Y

Tactic:
exact preservesFiniteLimits_of_natIso e

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ rightExactFunctor C D F ↔ PreservesFiniteColimits F

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : rightExactFunctor C D X
⊢ PreservesFiniteColimits X

Tactic:
simp only [rightExactFunctor_iff] at h ⊢

Premises used: CategoryTheory.rightExactFunctor_iff
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : PreservesFiniteColimits X
⊢ PreservesFiniteColimits Y

Tactic:
preservesFiniteColimits_of_natIso e

Premises used: CategoryTheory.Limits.preservesFiniteColimits_of_natIso
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : Functor.{v₁, v₂, u₁, u₂} C D
e : X ≅ Y
h : PreservesFiniteColimits X
⊢ PreservesFiniteColimits Y

Tactic:
exact preservesFiniteColimits_of_natIso e

Premises used: CategoryTheory.Limits.preservesFiniteColimits_of_natIso
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ exactFunctor C D F ↔ PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Tactic:
Iff.rfl

Premises used: CategoryTheory.exactFunctor, CategoryTheory.leftExactFunctor, Iff.rfl, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := Functor.{v₁, v₂, u₁, u₂} C D)
    (leftExactFunctor C D ⊓ rightExactFunctor C D)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ LE.le (α := ObjectProperty (Functor.{v₁, v₂, u₁, u₂} C D)) (exactFunctor C D) (leftExactFunctor C D)

Tactic:
fun _ h ↦ h.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ LE.le (α := ObjectProperty (Functor.{v₁, v₂, u₁, u₂} C D)) (exactFunctor C D) (rightExactFunctor C D)

Tactic:
fun _ h ↦ h.2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ Functor.obj (ofExact C D) F =
    ObjectProperty.FullSubcategory.mk (P := leftExactFunctor C D) (F.obj (P := exactFunctor C D)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ Functor.obj (ofExact C D) F =
    ObjectProperty.FullSubcategory.mk (P := rightExactFunctor C D) (F.obj (P := exactFunctor C D)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ InducedCategory.Hom.hom (Functor.map (ofExact C D) α) = α.hom

Tactic:
rfl

Premises used: CategoryTheory.exactFunctor, CategoryTheory.leftExactFunctor, rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ InducedCategory.Hom.hom (Functor.map (ofExact C D) α) = α.hom

Tactic:
rfl

Premises used: CategoryTheory.exactFunctor, rfl, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ Functor.obj (forget C D) F = F.obj (P := leftExactFunctor C D)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ Functor.obj (forget C D) F = F.obj (P := rightExactFunctor C D)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ Functor.obj (forget C D) F = F.obj (P := exactFunctor C D)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ Functor.map (forget C D) α = α.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ Functor.map (forget C D) α = α.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ Functor.map (forget C D) α = α.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
⊢ leftExactFunctor C D F

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteColimits F
⊢ rightExactFunctor C D F

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
inst_3 : PreservesFiniteColimits F
left : PreservesFiniteLimits F
right : PreservesFiniteColimits F
⊢ PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
inst_3 : PreservesFiniteColimits F
⊢ PreservesFiniteLimits F

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
inst_3 : PreservesFiniteColimits F
⊢ PreservesFiniteColimits F

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
⊢ (of F).obj (P := leftExactFunctor C D) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteColimits F
⊢ (of F).obj (P := rightExactFunctor C D) = F

Tactic:
rfl

Premises used: rfl