awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Indization
Goal:
C : Type v
inst : SmallCategory C
inst_1 : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w : SmallCategory I
w_1 : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk (X := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)
i' : Arrow.mk (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f) ≅
  Arrow.mk (X := Abelian.coimage (P := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)) (Y :=
    Abelian.image (P := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ))
    (coimageImageComparison (Functor.map (Ind.lim I) ϕ)) :=
  Functor.mapIso coimageImageComparisonFunctor i
this : IsIso i'.hom
rw :
  IsIso (X := Functor.obj (Ind.lim I) (Abelian.coimage ϕ)) (Y := Functor.obj (Ind.lim I) (Abelian.image ϕ))
    (Functor.map (Ind.lim I) (coimageImageComparison ϕ))
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)

Tactic:
rw [Arrow.isIso_iff_isIso_of_isIso i'.hom,
    Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv]

Premises used: CategoryTheory.Arrow.isIso_iff_isIso_of_isIso, CategoryTheory.Ind.lim, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Abelian.PreservesCoimageImageComparison.iso
-- Module: Mathlib.CategoryTheory.Abelian.Indization
Goal:
C : Type v
inst : SmallCategory C
inst_1 : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w : SmallCategory I
w_1 : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk (X := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)
i' : Arrow.mk (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f) ≅
  Arrow.mk (X := Abelian.coimage (P := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)) (Y :=
    Abelian.image (P := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ))
    (coimageImageComparison (Functor.map (Ind.lim I) ϕ)) :=
  Functor.mapIso coimageImageComparisonFunctor i
this : IsIso i'.hom
⊢ IsIso (X := Functor.obj (Ind.lim I) (Abelian.coimage ϕ)) (Y := Functor.obj (Ind.lim I) (Abelian.image ϕ))
    (Functor.map (Ind.lim I) (coimageImageComparison ϕ))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : C
hJ : Injective.{v, u} J
this : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J) := ⋯
⊢ Functor.PreservesHomology.{v, u, v, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)

Tactic:
apply Functor.preservesHomology_of_preservesEpis_and_kernels

Premises used: CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : C
hP : Injective.{v, u} J
⊢ PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)

Tactic:
apply Functor.preservesFiniteColimits_of_preservesHomology

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

Tactic:
rw [injective_iff_preservesEpimorphisms_preadditive_yoneda_obj']

Premises used: CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj'
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : C
hP : PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
⊢ Functor.PreservesHomology.{v, u, v, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)

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

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : HasInjectiveDimensionLT.{v, u} X n
i : ℕ
hi : n ≤ i
Y : C
this : HasExt C := ⋯
⊢ ∀ ⦃Y : C⦄, Subsingleton (Ext Y X i)

Tactic:
have := hX.subsingleton' i hi
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : HasInjectiveDimensionLT.{v, u} X n
i : ℕ
hi : n ≤ i
Y : C
this_1 : HasExt C := ⋯
this : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X i)
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} Y X i)

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

Premises used: CategoryTheory.Abelian.Ext.chgUniv, Equiv.symm, Equiv.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : HasInjectiveDimensionLT.{v, u} X n
i : ℕ
hi : n ≤ i
Y : C
this_1 : HasExt C := ⋯
this : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X i)
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} Y X i)

Tactic:
exact Ext.chgUniv.{w, max u v}.symm.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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} Y X i), e = 0
i : ℕ
hi : n ≤ i
Y : C
e₁ e₂ : Ext.{w, v, u} Y X i
⊢ e₁ = e₂

Tactic:
simp only [hX i hi]
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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} Y X i), e = 0
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} Y X i)

Tactic:
have : Subsingleton (Ext Y X i) := ⟨fun e₁ e₂ ↦ by simp only [hX i hi]⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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} Y X i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this_1 : Subsingleton.{w + 1} (Ext.{w, v, u} Y X i)
this : HasExt C := ⋯
⊢ Subsingleton (Ext Y X i)

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

Premises used: CategoryTheory.Abelian.Ext.chgUniv, Equiv.symm, Equiv.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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} Y X i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this_1 : Subsingleton.{w + 1} (Ext.{w, v, u} Y X i)
this : HasExt C := ⋯
⊢ Subsingleton (Ext Y X i)

Tactic:
exact Ext.chgUniv.{max u v, w}.symm.subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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} Y X i
n : ℕ
inst_3 : HasInjectiveDimensionLT.{v, u} X n
hi : n ≤ i
⊢ e = 0

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

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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
⊢ HasInjectiveDimensionLT.{v, u} X n ↔ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X i), e = 0

Tactic:
⟨fun _ _ hi _ e ↦ e.eq_zero_of_hasInjectiveDimensionLT n hi,
    HasInjectiveDimensionLT.mk⟩

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.HasInjectiveDimensionLT.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 Y X i), e = 0
⊢ HasInjectiveDimensionLT.{v, u} X 0

Tactic:
rw [hasInjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasInjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 Y X i
rw : e.comp (Ext.mk₀ (𝟙 X)) ⋯ = 0
rw₁ : Eq (α := Ext Y X i) (e.comp (Ext.mk₀ 0) ⋯) 0
rw₂ : Eq (α := Ext Y X i) (e.comp 0 ⋯) 0
rw₃ rw₄ : Eq (α := Ext Y X i) 0 0
⊢ e = 0

Tactic:
rw [← e.comp_mk₀_id, hX.eq_zero_of_tgt (𝟙 X), Ext.mk₀_zero, Ext.comp_zero]

Premises used: CategoryTheory.Abelian.Ext.comp_zero, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.Ext.comp_mk₀_id, CategoryTheory.Abelian.Ext.mk₀_zero, CategoryTheory.Limits.IsZero.eq_zero_of_tgt
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ HasInjectiveDimensionLT.{v, u} (C := C) 0 0

Tactic:
(isZero_zero C).hasInjectiveDimensionLT_zero

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.hasInjectiveDimensionLT_zero
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasInjectiveDimensionLT.{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.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasInjectiveDimensionLT.{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₀
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasInjectiveDimensionLT.{v, u} X 0
this : HasExt C := ⋯
⊢ LE.le (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasInjectiveDimensionLT.{v, u} X 0
this : HasExt C := ⋯
⊢ 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)

Tactic:
simpa only [Ext.homEquiv₀_symm_apply, Ext.mk₀_zero]
    using Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT _ 0 (by rfl)

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.Abelian.Ext.mk₀_zero, OfNat.ofNat, CategoryTheory.Abelian.Ext.homEquiv₀_symm_apply
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ HasInjectiveDimensionLT.{v, u} X 0 ↔ IsZero.{v, u} X

Tactic:
⟨fun _ ↦ isZero_of_hasInjectiveDimensionLT_zero X, fun h ↦ h.hasInjectiveDimensionLT_zero⟩

Premises used: CategoryTheory.Limits.IsZero.hasInjectiveDimensionLT_zero, CategoryTheory.isZero_of_hasInjectiveDimensionLT_zero, Iff.intro
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n m : ℕ
h : n ≤ m
inst_2 : HasInjectiveDimensionLT.{v, u} X n
this : HasExt C := ⋯
rw : ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
⊢ HasInjectiveDimensionLT.{v, u} X m

Tactic:
rw [hasInjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasInjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n m : ℕ
h : n ≤ m
inst_2 : HasInjectiveDimensionLT.{v, u} X n
this : HasExt C := ⋯
i : ℕ
hi : m ≤ i
Y : C
e : Ext Y X i
⊢ n ≤ i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n m : ℕ
h : n ≤ m
inst_2 : HasInjectiveDimensionLT.{v, u} X n
this : HasExt C := ⋯
i : ℕ
hi : m ≤ i
Y : C
e : Ext Y X i
⊢ e = 0

Tactic:
exact e.eq_zero_of_hasInjectiveDimensionLT n (by lia)

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} X n
k : ℕ
⊢ n ≤ n + k

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} X n
k : ℕ
⊢ n ≤ k + n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} X n
⊢ HasInjectiveDimensionLT.{v, u} X n.succ

Tactic:
inferInstanceAs (HasInjectiveDimensionLT X (n + 1))

Premises used: _private.0.CategoryTheory.instHasInjectiveDimensionLTSucc._proof_1
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Injective.{v, u} X
this : HasExt C := ⋯
rw : ∀ (i : ℕ), 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
⊢ HasInjectiveDimensionLT.{v, u} X 1

Tactic:
rw [hasInjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasInjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Injective.{v, u} X
this : HasExt C := ⋯
i : ℕ
hi : 1 ≤ i
Y : C
e : Ext Y X i
zero : ∀ (hi : LE.le (α := ℕ) 1 0) (e : Ext Y X 0), e = 0
succ : ∀ (i : ℕ) (hi : 1 ≤ i + 1) (e : Ext Y X (i + 1)), e = 0
⊢ e = 0

Tactic:
obtain _ | i := i
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Injective.{v, u} X
this : HasExt C := ⋯
Y : C
hi : LE.le (α := ℕ) 1 0
e : Ext Y X 0
⊢ e = 0

Tactic:
simp at hi
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Injective.{v, u} X
this : HasExt C := ⋯
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext Y X (i + 1)
⊢ e = 0

Tactic:
e.eq_zero_of_injective

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_injective
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Injective.{v, u} X
this : HasExt C := ⋯
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext Y X (i + 1)
⊢ e = 0

Tactic:
exact e.eq_zero_of_injective

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_injective
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : Injective.{v, u} X
⊢ LE.le (α := ℕ) 1 1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
refine :
  ∀ (h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} Y X 1)) {X_1 Y : C} (f : X_1 ⟶ X) (g : X_1 ⟶ Y),
    Mono g → ∃ (h : Y ⟶ X), g ≫ h = f
⊢ Injective.{v, u} X ↔ ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} Y X 1)

Tactic:
refine ⟨fun h ↦ HasInjectiveDimensionLT.subsingleton X 1 1 (by rfl),
    fun h ↦ ⟨fun f g _ ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} Y X 1)
X_1 Y : C
f : X_1 ⟶ X
g : X_1 ⟶ Y
h_1 : Mono g
⊢ Eq.{w + 1} (α :=
    Ext.{w, v, u}
      (ShortComplex.X₃
        { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C })
      X 1)
    (Ext.comp (ShortComplex.ShortExact.extClass ⋯) (Ext.mk₀ f) ⋯) 0

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} Y X 1)
X_1 Y : C
f : X_1 ⟶ X
g : X_1 ⟶ Y
h_1 : Mono g
obtain :
  ∀
    (φ :
      Ext.{w, v, u}
        (ShortComplex.X₂
          { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C })
        X 0)
    (hφ :
      Ext.comp
          (Ext.mk₀
            (ShortComplex.f
              { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C }))
          φ ⋯ =
        Ext.mk₀ f),
    ∃ (h : Y ⟶ X), g ≫ h = f
⊢ ∃ (h : Y ⟶ X), g ≫ h = f

Tactic:
obtain ⟨φ, hφ⟩ := Ext.contravariant_sequence_exact₁ { exact := ShortComplex.exact_cokernel g } _
    (Ext.mk₀ f) (zero_add 1) (by subsingleton)

Premises used: CategoryTheory.ShortComplex.exact_cokernel, zero_add, CategoryTheory.ShortComplex.ShortExact.mk, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁, OfNat.ofNat, CategoryTheory.Abelian.Ext.mk₀
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} Y X 1)
X_1 Y : C
f : X_1 ⟶ X
g : X_1 ⟶ Y
h_1 : Mono g
φ :
  Ext.{w, v, u}
    (ShortComplex.X₂
      { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C })
    X 0
hφ :
  Ext.comp
      (Ext.mk₀
        (ShortComplex.f
          { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C }))
      φ ⋯ =
    Ext.mk₀ f
obtain :
  ∀
    (φ :
      ShortComplex.X₂
          { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C } ⟶
        X)
    (hφ :
      Eq.{w + 1} (α :=
        Ext.{w, v, u}
          (ShortComplex.X₁
            { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C })
          X 0)
        (Ext.comp
          (Ext.mk₀
            (ShortComplex.f
              { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C }))
          ((Equiv.symm Ext.homEquiv₀ :
              (a : { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ ⟶ X) →
                Ext { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ X 0)
            φ)
          ⋯)
        (Ext.mk₀ f)),
    ∃ (h : Y ⟶ X), g ≫ h = f
⊢ ∃ (h : Y ⟶ X), g ≫ h = f

Tactic:
obtain ⟨φ, rfl⟩ := Ext.homEquiv₀.symm.surjective φ

Premises used: Equiv.surjective, Equiv.symm, CategoryTheory.Abelian.Ext.homEquiv₀, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} Y X 1)
X_1 Y : C
f : X_1 ⟶ X
g : X_1 ⟶ Y
h_1 : Mono g
φ :
  ShortComplex.X₂
      { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C } ⟶
    X
hφ :
  Eq.{w + 1} (α :=
    Ext.{w, v, u}
      (ShortComplex.X₁
        { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C })
      X 0)
    (Ext.comp
      (Ext.mk₀
        (ShortComplex.f
          { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C }))
      ((Equiv.symm Ext.homEquiv₀ :
          (a : { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ ⟶ X) →
            Ext { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ X 0)
        φ)
      ⋯)
    (Ext.mk₀ f)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X_1 X 0)
    ((Equiv.symm Ext.homEquiv₀ : (a : X_1 ⟶ X) → Ext X_1 X 0) (g ≫ φ) : Ext.{w, v, u} X_1 X 0)
    ((Equiv.symm Ext.homEquiv₀ : (a : X_1 ⟶ X) → Ext X_1 X 0) f : Ext.{w, v, u} X_1 X 0)

Tactic:
simpa using hφ
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} Y X 1)
X_1 Y : C
f : X_1 ⟶ X
g : X_1 ⟶ Y
h_1 : Mono g
φ :
  ShortComplex.X₂
      { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C } ⟶
    X
hφ :
  Eq.{w + 1} (α :=
    Ext.{w, v, u}
      (ShortComplex.X₁
        { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C })
      X 0)
    (Ext.comp
      (Ext.mk₀
        (ShortComplex.f
          { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ : ShortComplex.{v, u} C }))
      ((Equiv.symm Ext.homEquiv₀ :
          (a : { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ ⟶ X) →
            Ext { X₁ := X_1, X₂ := Y, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ X 0)
        φ)
      ⋯)
    (Ext.mk₀ f)
⊢ ∃ (h : Y ⟶ X), g ≫ h = f

Tactic:
exact ⟨φ, Ext.homEquiv₀.symm.injective (by simpa using hφ)⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
this : HasExt C := ⋯
h : HasInjectiveDimensionLT.{v, u} X 1
⊢ LE.le (α := ℕ) 1 1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
this : HasExt C := ⋯
⊢ Injective.{v, u} X ↔ HasInjectiveDimensionLT.{v, u} X 1

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ injective_iff_subsingleton_ext_one.2
    (HasInjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} X 1
⊢ Injective.{v, u} X

Tactic:
injective_iff_hasInjectiveDimensionLT_one.mpr ‹_›

Premises used: Iff.mpr, CategoryTheory.injective_iff_hasInjectiveDimensionLT_one
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
h : Retract X Y
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} Y n
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
⊢ HasInjectiveDimensionLT.{v, u} X n

Tactic:
rw [hasInjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasInjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
h : Retract X Y
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} Y n
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
rw : x.comp (Ext.mk₀ (𝟙 X)) ⋯ = 0
rw₁ : x.comp (Ext.mk₀ (h.i ≫ h.r)) ⋯ = 0
rw₂ : x.comp (Ext.comp (Ext.mk₀ h.i) (Ext.mk₀ h.r) ⋯) ⋯ = 0
rw₃ : (x.comp (Ext.mk₀ h.i) ⋯).comp (Ext.mk₀ h.r) ⋯ = 0
rw₄ : Eq (α := Ext T X i) (Ext.comp 0 (Ext.mk₀ h.r) ⋯) 0
rw₅ rw₆ : Eq (α := Ext T X i) 0 0
⊢ x = 0

Tactic:
rw [← x.comp_mk₀_id, ← h.retract, ← Ext.mk₀_comp_mk₀, ← Ext.comp_assoc_of_second_deg_zero,
    (x.comp (Ext.mk₀ h.i) (add_zero i)).eq_zero_of_hasInjectiveDimensionLT n hi, Ext.zero_comp]

Premises used: CategoryTheory.Abelian.Ext.zero_comp, CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.Retract.retract, CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, CategoryTheory.Abelian.Ext.comp_mk₀_id, CategoryTheory.Retract.i, CategoryTheory.Abelian.Ext.comp, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀, add_zero, CategoryTheory.Abelian.Ext.mk₀