awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ : Preradical.{u_2, u_1} C
X : C
⊢ Eq (α := Φ.r.obj X ⟶ Φ.quotient.obj X) (Φ.ι.app X ≫ NatTrans.app Φ.π X) 0

Tactic:
simp [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
dsimp : Mono (Φ.ι.app X)
⊢ Mono (X := ShortComplex.X₁ (Φ.shortComplexObj X)) (ShortComplex.f (Φ.shortComplexObj X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ Mono (Φ.ι.app X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
dsimp : Epi (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X)
⊢ Epi (X := ShortComplex.X₂ (Φ.shortComplexObj X)) (ShortComplex.g (Φ.shortComplexObj X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ Epi (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
⊢ Epi (X := (Φ.colon Ψ).r) (pullback.snd Φ.π (Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ Epi (X := (Φ.colon Ψ).r.obj X) (NatTrans.app (Φ.colonπ Ψ) X)

Tactic:
instEpiAppOfFunctor (Φ.colonπ Ψ) X

Premises used: CategoryTheory.Abelian.Preradical.colonπ, CategoryTheory.instEpiAppOfFunctor
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
⊢ IsPullback (Φ.colon Ψ).ι (Φ.colonπ Ψ) Φ.π (Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom)

Tactic:
.of_hasPullback _ _

Premises used: CategoryTheory.Abelian.Preradical.colonπ, CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ IsPullback ((Φ.colon Ψ).ι.app X) (NatTrans.app (Φ.colonπ Ψ) X) (NatTrans.app Φ.π X) (Ψ.ι.app (Φ.quotient.obj X))

Tactic:
simpa using (isPullback_colon Φ Ψ).map ((evaluation _ _).obj X)

Premises used: CategoryTheory.evaluation, CategoryTheory.Abelian.Preradical.isPullback_colon, CategoryTheory.IsPullback.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ (Φ.colon Ψ).ι.app X ≫ NatTrans.app Φ.π X = NatTrans.app (Φ.colonπ Ψ) X ≫ Ψ.ι.app (Φ.quotient.obj X)

Tactic:
(isPullback_colon_obj Φ Ψ X).w

Premises used: CategoryTheory.Abelian.Preradical.isPullback_colon_obj, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
⊢ Φ.ι ≫ Φ.π = 0 ≫ Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
⊢ Eq (α := Φ.obj (P := Over.isMono (𝟭 C)).left ⟶ Φ.quotient ⋙ Ψ.r)
    (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ)) ≫ Φ.colonπ Ψ) 0

Tactic:
simp [toColon]

Premises used: CategoryTheory.Abelian.Preradical.toColon
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
⊢ Eq (α := Φ.obj (P := Over.isMono (𝟭 C)).left.obj X ⟶ (Φ.quotient ⋙ Ψ.r).obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ NatTrans.app (Φ.colonπ Ψ) X) 0

Tactic:
NatTrans.congr_app (toColon_hom_left_colonπ Φ Ψ) X

Premises used: CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ, CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
rw : (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ)) ≫ (Φ.colon Ψ).ι).app X = Φ.ι.app X
rw₁ rw₂ : Φ.obj (P := Over.isMono (𝟭 C)).hom.app X = Φ.ι.app X
⊢ NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ (Φ.colon Ψ).ι.app X = Φ.ι.app X

Tactic:
rw [← NatTrans.comp_app, Over.w]

Premises used: CategoryTheory.Over.w, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
mp :
  IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
      (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X) →
    IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
mpr :
  IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X)) →
    IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
      (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
      (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X) ↔
    IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h :
  IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
⊢ Eq (α := Φ.obj (P := Over.isMono (𝟭 C)).left.obj X ⟶ (Φ.quotient ⋙ Ψ.r).obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ NatTrans.app (Φ.colonπ Ψ) X) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h :
  IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
⊢ IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))

Tactic:
exact IsZero.of_epi_eq_zero ((colonπ Φ Ψ).app X)
      (zero_of_epi_comp ((toColon Φ Ψ).hom.left.app X) (by simp))

Premises used: CategoryTheory.Abelian.Preradical.colonπ, CategoryTheory.Limits.zero_of_epi_comp, CategoryTheory.Over.Hom.left, CategoryTheory.Abelian.Preradical.toColon, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Limits.IsZero.of_epi_eq_zero, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
rw : Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) (NatTrans.app (Φ.colonπ Ψ) X ≫ Ψ.ι.app (Φ.quotient.obj X)) 0
rw₁ : Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) (0 ≫ Ψ.ι.app (Φ.quotient.obj X)) 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) 0 0
⊢ Eq (α := (Φ.colon Ψ).r.obj X ⟶ Φ.quotient.obj X) ((Φ.colon Ψ).ι.app X ≫ NatTrans.app Φ.π X) 0

Tactic:
rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp]

Premises used: CategoryTheory.Abelian.Preradical.colonπ, CategoryTheory.Abelian.Preradical.colon_ι_app_π_app, CategoryTheory.Limits.IsZero.eq_zero_of_tgt, CategoryTheory.Limits.zero_comp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
mpr :
  ∀
    (inv :
      (Φ.colon Ψ).r.obj X ⟶
        Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) ⋯))
    (hinv : inv ≫ Fork.ι (KernelFork.ofι (Φ.ι.app X) ⋯) = (Φ.colon Ψ).ι.app X),
    IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
      (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)

Tactic:
obtain ⟨inv, hinv⟩ :=
      KernelFork.IsLimit.lift' (Φ.isLimitKernelForkObj X) ((colon Φ Ψ).ι.app X) (by
        rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp])

Premises used: CategoryTheory.Abelian.Preradical.isLimitKernelForkObj, CategoryTheory.Limits.KernelFork.IsLimit.lift', CategoryTheory.inv, CategoryTheory.NatTrans.app, CategoryTheory.Abelian.Preradical.colon, CategoryTheory.Abelian.Preradical.ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
inv :
  (Φ.colon Ψ).r.obj X ⟶
    Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) ⋯)
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)

Tactic:
⟨inv, ?_, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
inv :
  (Φ.colon Ψ).r.obj X ⟶
    Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) ⋯)
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
mpr :
  NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ inv =
    𝟙 (Φ.obj (P := Over.isMono (𝟭 C)).left.obj X)
mpr₁ :
  inv ≫ NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X =
    𝟙 ((Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)

Tactic:
refine ⟨inv, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
inv :
  (Φ.colon Ψ).r.obj X ⟶
    Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) ⋯)
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
⊢ NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ inv =
    𝟙 (Φ.obj (P := Over.isMono (𝟭 C)).left.obj X)

Tactic:
simp [← cancel_mono (Φ.ι.app X), hinv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.NatTrans.app, CategoryTheory.Abelian.Preradical.ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
inv :
  (Φ.colon Ψ).r.obj X ⟶
    Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) ⋯)
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
⊢ inv ≫ NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X =
    𝟙 ((Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)

Tactic:
simp [← cancel_mono ((Φ.colon Ψ).ι.app X), hinv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.NatTrans.app, CategoryTheory.Abelian.Preradical.colon, CategoryTheory.Abelian.Preradical.ι
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
⊢ IsIso (Y := Φ.colon Ψ) (Φ.toColon Ψ) ↔ IsZero (Φ.quotient ⋙ Ψ.r)

Tactic:
simpa [MonoOver.isIso_iff_isIso_hom_left, isZero_iff (Φ.quotient ⋙ Ψ.r),
    NatTrans.isIso_iff_isIso_app] using forall_congr' fun x ↦ isIso_toColon_hom_left_app_iff

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Abelian.Preradical.quotient, CategoryTheory.Abelian.Preradical.r, CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.Functor.isZero_iff, CategoryTheory.Abelian.Preradical.isIso_toColon_hom_left_app_iff, CategoryTheory.MonoOver.isIso_iff_isIso_hom_left, forall_congr'
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Preradical.{v_1, u_1} C
⊢ isRadical C Φ ↔ IsIso (Y := Φ.colon Φ) (Φ.toColon Φ)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.Abelian.Preradical.isRadical
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Preradical.{v_1, u_1} C
rw : IsIso (Y := Φ.colon Φ) (Φ.toColon Φ) ↔ IsZero (Φ.quotient ⋙ Φ.r)
rw₁ rw₂ : IsZero (Φ.quotient ⋙ Φ.r) ↔ IsZero (Φ.quotient ⋙ Φ.r)
⊢ isRadical C Φ ↔ IsZero (Φ.quotient ⋙ Φ.r)

Tactic:
rw [isRadical_iff_isIso, isIso_toColon_iff]

Premises used: CategoryTheory.Abelian.Preradical.isRadical_iff_isIso, CategoryTheory.Abelian.Preradical.isIso_toColon_iff
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Radical.{v_1, u_1} C
⊢ IsIso (Y := Φ.obj (P := Preradical.isRadical C).colon (Φ.obj (P := Preradical.isRadical C)))
    (Φ.obj (P := Preradical.isRadical C).toColon (Φ.obj (P := Preradical.isRadical C)))

Tactic:
Φ.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Abelian.Preradical.isRadical
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Radical.{v_1, u_1} C
rw :
  IsIso (Y := Φ.obj (P := Preradical.isRadical C).colon (Φ.obj (P := Preradical.isRadical C)))
    (Φ.obj (P := Preradical.isRadical C).toColon (Φ.obj (P := Preradical.isRadical C)))
⊢ IsZero (Φ.obj (P := Preradical.isRadical C).quotient ⋙ Φ.obj (P := Preradical.isRadical C).r)

Tactic:
rw [← Preradical.isRadical_iff_isZero, Preradical.isRadical_iff_isIso]

Premises used: CategoryTheory.Abelian.Preradical.isRadical_iff_isZero, CategoryTheory.Abelian.Preradical.isRadical_iff_isIso
-- Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Radical.{v_1, u_1} C
⊢ IsIso (Y := Φ.obj (P := Preradical.isRadical C).colon (Φ.obj (P := Preradical.isRadical C)))
    (Φ.obj (P := Preradical.isRadical C).toColon (Φ.obj (P := Preradical.isRadical C)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : Projective.{v, u} P
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
haveI := (projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj P).mp hP
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : Projective.{v, u} P
this : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Functor.PreservesHomology.{v, u, v, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
apply Functor.preservesHomology_of_preservesEpis_and_kernels

Premises used: CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : Projective.{v, u} P
⊢ PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
apply Functor.preservesFiniteColimits_of_preservesHomology

Premises used: CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
rw : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Projective.{v, u} P

Tactic:
rw [projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj]

Premises used: CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Functor.PreservesHomology.{v, u, v, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
have := Functor.preservesHomologyOfExact (preadditiveCoyonedaObj P)
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
this : Functor.PreservesHomology.{v, u, v, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : HasProjectiveDimensionLT.{v, u} X n
i : ℕ
hi : n ≤ i
Y : C
this : HasExt C := ⋯
⊢ ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)

Tactic:
have := hX.subsingleton' i hi
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : HasProjectiveDimensionLT.{v, u} X n
i : ℕ
hi : n ≤ i
Y : C
this_1 : HasExt C := ⋯
this : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} X Y i)

Tactic:
Ext.chgUniv.{w, max u v}.symm.subsingleton

Premises used: CategoryTheory.Abelian.Ext.chgUniv, Equiv.symm, Equiv.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : HasProjectiveDimensionLT.{v, u} X n
i : ℕ
hi : n ≤ i
Y : C
this_1 : HasExt C := ⋯
this : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} X Y i)

Tactic:
exact Ext.chgUniv.{w, max u v}.symm.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
e₁ e₂ : Ext.{w, v, u} X Y i
⊢ e₁ = e₂

Tactic:
simp only [hX i hi]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} X Y i)

Tactic:
have : Subsingleton (Ext X Y i) := ⟨fun e₁ e₂ ↦ by simp only [hX i hi]⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this_1 : Subsingleton.{w + 1} (Ext.{w, v, u} X Y i)
this : HasExt C := ⋯
⊢ Subsingleton (Ext X Y i)

Tactic:
Ext.chgUniv.{max u v, w}.symm.subsingleton

Premises used: CategoryTheory.Abelian.Ext.chgUniv, Equiv.symm, Equiv.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this_1 : Subsingleton.{w + 1} (Ext.{w, v, u} X Y i)
this : HasExt C := ⋯
⊢ Subsingleton (Ext X Y i)

Tactic:
exact Ext.chgUniv.{max u v, w}.symm.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
i : ℕ
e : Ext.{w, v, u} X Y i
n : ℕ
inst_3 : HasProjectiveDimensionLT.{v, u} X n
hi : n ≤ i
⊢ e = 0

Tactic:
(HasProjectiveDimensionLT.subsingleton X n i hi Y).elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasExt.{w, v, u} C
⊢ HasProjectiveDimensionLT.{v, u} X n ↔ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y i), e = 0

Tactic:
⟨fun _ _ hi _ e ↦ e.eq_zero_of_hasProjectiveDimensionLT n hi,
    HasProjectiveDimensionLT.mk⟩

Premises used: Iff.intro, CategoryTheory.HasProjectiveDimensionLT.mk, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hX : IsZero.{v, u} X
this : HasExt C := ⋯
rw : ∀ (i : ℕ), 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
⊢ HasProjectiveDimensionLT.{v, u} X 0

Tactic:
rw [hasProjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasProjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hX : IsZero.{v, u} X
this : HasExt C := ⋯
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
rw : Ext.comp (Ext.mk₀ (𝟙 X)) e ⋯ = 0
rw₁ : Eq (α := Ext X Y i) (Ext.comp (Ext.mk₀ 0) e ⋯) 0
rw₂ : Eq (α := Ext X Y i) (Ext.comp 0 e ⋯) 0
rw₃ rw₄ : Eq (α := Ext X Y i) 0 0
⊢ e = 0

Tactic:
rw [← e.mk₀_id_comp, hX.eq_of_src (𝟙 X) 0, Ext.mk₀_zero, Ext.zero_comp]

Premises used: CategoryTheory.Abelian.Ext.zero_comp, CategoryTheory.Abelian.Ext.mk₀_id_comp, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.Ext.mk₀_zero, CategoryTheory.Limits.IsZero.eq_of_src, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ HasProjectiveDimensionLT.{v, u} (C := C) 0 0

Tactic:
(isZero_zero C).hasProjectiveDimensionLT_zero

Premises used: CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero, CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasProjectiveDimensionLT.{v, u} X 0
this : HasExt C := ⋯
rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ IsZero.{v, u} X

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasProjectiveDimensionLT.{v, u} X 0
this : HasExt C := ⋯
a :
  Eq (α := Ext X X 0) ((Equiv.symm Ext.homEquiv₀ : (a : X ⟶ X) → Ext X X 0) (𝟙 X) : Ext X X 0)
    ((Equiv.symm Ext.homEquiv₀ : (a : X ⟶ X) → Ext X X 0) 0 : Ext X X 0)
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
apply Ext.homEquiv₀.symm.injective

Premises used: Equiv.injective, Equiv.symm, CategoryTheory.Abelian.Ext.homEquiv₀