awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : L.PreservesMonomorphisms
adj : L ⊣ R
J : D
inst_3 : Injective.{v₂, u₂} J
A x : C
g : A ⟶ R.obj J
f : A ⟶ x
im : Mono f
⊢ Eq.{v₂ + 1} (α := L.obj A ⟶ J)
    (((adj.homEquiv A J).symm : (a : A ⟶ R.obj J) → L.obj A ⟶ J)
        (f ≫
          (adj.homEquiv x J : (a : L.obj x ⟶ J) → x ⟶ R.obj J)
            (factorThru (((adj.homEquiv A J).symm : (a : A ⟶ R.obj J) → L.obj A ⟶ J) g) (L.map f))) :
      L.obj A ⟶ J)
    (((adj.homEquiv A J).symm : (a : A ⟶ R.obj J) → L.obj A ⟶ J) g : L.obj A ⟶ J)

Tactic:
simp [Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.homEquiv_counit
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
pos : ∀ (h : IsZero.{v₁, u₁} X), ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
neg : ∀ (h : ¬IsZero.{v₁, u₁} X), ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
⊢ ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J

Tactic:
by_cases h : IsZero X

Premises used: CategoryTheory.Limits.IsZero
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
h : IsZero.{v₁, u₁} X
⊢ Injective.{v₁, u₁} X

Tactic:
have := h.injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
h : IsZero.{v₁, u₁} X
this : Injective.{v₁, u₁} X
tauto tauto₁ tauto₂ :
  IsZero.{v₁, u₁} X →
    IsZero.{v₁, u₁}
      (InjectivePresentation.J.{v₁, u₁}
        { J := X, injective := ⋯, f := 𝟙 X, mono := ⋯ : InjectivePresentation.{v₁, u₁} X })
⊢ IsZero.{v₁, u₁} X →
    IsZero.{v₁, u₁}
      (InjectivePresentation.J.{v₁, u₁}
        { J := X, injective := ⋯, f := 𝟙 X, mono := ⋯ : InjectivePresentation.{v₁, u₁} X })

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
h : IsZero.{v₁, u₁} X
this : Injective.{v₁, u₁} X
⊢ ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J

Tactic:
exact ⟨{ J := X, f := 𝟙 X}, by tauto⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
h : ¬IsZero.{v₁, u₁} X
tauto : IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} (InjectivePresentation.J.{v₁, u₁} (Nonempty.some ⋯))
⊢ IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} (InjectivePresentation.J.{v₁, u₁} (Nonempty.some ⋯))

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
h : ¬IsZero.{v₁, u₁} X
⊢ ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J

Tactic:
exact ⟨(EnoughInjectives.presentation X).some, by tauto⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
⊢ Injective.{v₁, u₁} (under.{v₁, u₁} X)

Tactic:
(exists_presentation X).choose.injective

Premises used: CategoryTheory.InjectivePresentation.injective, CategoryTheory.Injective.exists_presentation, CategoryTheory.Injective.under, Exists.choose
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
⊢ Mono.{v₁, u₁} (Y := under.{v₁, u₁} X) (ι X)

Tactic:
(exists_presentation X).choose.mono

Premises used: CategoryTheory.InjectivePresentation.mono, CategoryTheory.Injective.exists_presentation, CategoryTheory.Injective.under, Exists.choose, CategoryTheory.Injective.ι
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
hX : IsZero.{v₁, u₁} X
⊢ IsZero.{v₁, u₁} (under.{v₁, u₁} X)

Tactic:
(exists_presentation X).choose_spec hX

Premises used: Exists.choose_spec, CategoryTheory.Injective.exists_presentation, CategoryTheory.Injective.under
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
⊢ EnoughProjectives.{v₁, u₁} Cᵒᵖ

Tactic:
⟨fun X => ⟨{ p := _, f := (Injective.ι (unop X)).op}⟩⟩

Premises used: Quiver.Hom.op, Nonempty.intro, CategoryTheory.ProjectivePresentation.mk, Opposite.op, CategoryTheory.Injective.under, Opposite.unop, CategoryTheory.EnoughProjectives.mk, CategoryTheory.Injective.ι
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughProjectives.{v₁, u₁} C
⊢ EnoughInjectives.{v₁, u₁} Cᵒᵖ

Tactic:
⟨fun X => ⟨⟨_, inferInstance, (Projective.π (unop X)).op, inferInstance⟩⟩⟩

Premises used: CategoryTheory.Projective.over, CategoryTheory.Projective.π, Quiver.Hom.op, CategoryTheory.InjectivePresentation.mk, inferInstance, Nonempty.intro, CategoryTheory.EnoughInjectives.mk, Opposite.op, Opposite.unop
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} Cᵒᵖ
⊢ EnoughProjectives.{v₁, u₁} C

Tactic:
⟨fun X => ⟨{ p := _, f := (Injective.ι (op X)).unop} ⟩⟩

Premises used: Quiver.Hom.unop, Nonempty.intro, CategoryTheory.ProjectivePresentation.mk, Opposite.op, CategoryTheory.Injective.under, Opposite.unop, CategoryTheory.EnoughProjectives.mk, CategoryTheory.Injective.ι
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughProjectives.{v₁, u₁} Cᵒᵖ
⊢ EnoughInjectives.{v₁, u₁} C

Tactic:
⟨fun X => ⟨⟨_, inferInstance, (Projective.π (op X)).unop, inferInstance⟩⟩⟩

Premises used: CategoryTheory.Projective.over, CategoryTheory.Projective.π, CategoryTheory.InjectivePresentation.mk, Quiver.Hom.unop, inferInstance, Nonempty.intro, CategoryTheory.EnoughInjectives.mk, Opposite.op, Opposite.unop
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
I : D
hI : Injective.{v_1, u_1} I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst_3 : Mono g
rcases : ∀ (w : F.obj Y ⟶ I) (h : F.map g ≫ w = F.map f ≫ adj.counit.app I), ∃ (h : Y ⟶ G.obj I), g ≫ h = f
⊢ ∃ (h : Y ⟶ G.obj I), g ≫ h = f

Tactic:
rcases hI.factors (F.map f ≫ adj.counit.app _) (F.map g) with ⟨w,h⟩

Premises used: CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.app, CategoryTheory.Injective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
I : D
hI : Injective.{v_1, u_1} I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst_3 : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
h₁ : g ≫ adj.unit.app Y ≫ G.map w = f
⊢ ∃ (h : Y ⟶ G.obj I), g ≫ h = f

Tactic:
use adj.unit.app Y ≫ G.map w

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
I : D
hI : Injective.{v_1, u_1} I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst_3 : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
h₁ : adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app I) = f
⊢ g ≫ adj.unit.app Y ≫ G.map w = f

Tactic:
rw [← unit_naturality_assoc, ← G.map_comp, h]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
I : D
hI : Injective.{v_1, u_1} I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst_3 : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app I) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
⊢ PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G

Tactic:
haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
rcases : ∀ (w : G.obj Y ⟶ G.obj I) (h : G.map g ≫ w = G.map f), ∃ (h : Y ⟶ I), g ≫ h = f
⊢ ∃ (h : Y ⟶ I), g ≫ h = f

Tactic:
rcases hI.factors (G.map f) (G.map g) with ⟨w,h⟩

Premises used: CategoryTheory.Functor.map, CategoryTheory.Injective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
h₁ : g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I = f
⊢ ∃ (h : Y ⟶ I), g ≫ h = f

Tactic:
use inv (adj.counit.app _) ≫ F.map w ≫ adj.counit.app _

Premises used: CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ G.map (g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I) = G.map f

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I = f

Tactic:
exact G.map_injective (by simpa)

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
X : D
I : InjectivePresentation.{v_1, u_1} X
⊢ PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G

Tactic:
haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
X : D
I : InjectivePresentation.{v_1, u_1} X
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
⊢ Mono (G.map I.f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesMonomorphisms
I : C
hI : Injective.{v_1, u_1} (F.obj I)
X Y : C
g : X ⟶ I
f : X ⟶ Y
h : Mono f
obtain : ∀ (h : F.obj Y ⟶ F.obj I) (fac : F.map f ≫ h = F.map g), ∃ (h : Y ⟶ I), f ≫ h = g
⊢ ∃ (h : Y ⟶ I), f ≫ h = g

Tactic:
obtain ⟨h, fac⟩ := hI.factors (F.map g) (F.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Injective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesMonomorphisms
I : C
hI : Injective.{v_1, u_1} (F.obj I)
X Y : C
g : X ⟶ I
f : X ⟶ Y
h_1 : Mono f
h : F.obj Y ⟶ F.obj I
fac : F.map f ≫ h = F.map g
⊢ F.map (f ≫ F.preimage h) = F.map g

Tactic:
simp [fac]
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesMonomorphisms
I : C
hI : Injective.{v_1, u_1} (F.obj I)
X Y : C
g : X ⟶ I
f : X ⟶ Y
h_1 : Mono f
h : F.obj Y ⟶ F.obj I
fac : F.map f ≫ h = F.map g
⊢ ∃ (h : Y ⟶ I), f ≫ h = g

Tactic:
exact ⟨F.preimage h, F.map_injective (by simp [fac])⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
e : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : e.IsEquivalence
inst_3 : EnoughInjectives.{v₂, u₂} D
⊢ EnoughInjectives.{v₁, u₁} C

Tactic:
EnoughInjectives.of_adjunction (adj := e.asEquivalence.toAdjunction)

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.EnoughInjectives.of_adjunction
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Equivalence.{v₁, v_1, u₁, u_1} C D
P : C
⊢ Injective.{v_1, u_1} (F.functor.obj P) ↔ Injective.{v₁, u₁} P

Tactic:
⟨F.symm.toAdjunction.injective_of_map_injective P, F.symm.toAdjunction.map_injective P⟩

Premises used: CategoryTheory.Adjunction.map_injective, Iff.intro, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.injective_of_map_injective, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Equivalence.{v₁, v_1, u₁, u_1} C D
⊢ EnoughInjectives.{v₁, u₁} C ↔ EnoughInjectives.{v_1, u_1} D

Tactic:
⟨fun h => h.of_adjunction F.symm.toAdjunction, fun h => h.of_adjunction F.toAdjunction⟩

Premises used: Iff.intro, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Equivalence.symm, CategoryTheory.EnoughInjectives.of_adjunction
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
⊢ Injective.{v₁, u₁} X

Tactic:
Injective.mk (fun {A B} f e _ ↦ ?_)

Premises used: CategoryTheory.Injective.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
refine : ∀ {A B : C} (f : A ⟶ X) (e : A ⟶ B), Mono e → ∃ (h : B ⟶ X), e ≫ h = f
⊢ Injective.{v₁, u₁} X

Tactic:
refine Injective.mk (fun {A B} f e _ ↦ ?_)

Premises used: CategoryTheory.Injective.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
A B : C
f : A ⟶ X
e : A ⟶ B
h_1 : Mono e
rcases : ∀ (g : B ⟶ Y) (hg : e ≫ g = f ≫ h.i), ∃ (h : B ⟶ X), e ≫ h = f
⊢ ∃ (h : B ⟶ X), e ≫ h = f

Tactic:
rcases i.factors (f ≫ h.i) e with ⟨g, hg⟩

Premises used: CategoryTheory.Retract.i, CategoryTheory.CategoryStruct.comp, CategoryTheory.Injective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
A B : C
f : A ⟶ X
e : A ⟶ B
h_1 : Mono e
g : B ⟶ Y
hg : e ≫ g = f ≫ h.i
h₁ : e ≫ g ≫ h.r = f
⊢ ∃ (h : B ⟶ X), e ≫ h = f

Tactic:
use g ≫ h.r

Premises used: CategoryTheory.Retract.r
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
A B : C
f : A ⟶ X
e : A ⟶ B
h_1 : Mono e
g : B ⟶ Y
hg : e ≫ g = f ≫ h.i
⊢ e ≫ g ≫ h.r = f

Tactic:
simp [Category.assoc', hg]

Premises used: CategoryTheory.Category.assoc'
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
A B I : C
i : A ⟶ B
inst_1 : Mono i
inst_2 : Injective.{v, u} I
inst_3 : HasZeroObject.{v, u} C
p : I ⟶ 0
⊢ HasLiftingProperty i p

Tactic:
Injective.hasLiftingProperty_of_isZero i p (isZero_zero C)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Injective.hasLiftingProperty_of_isZero
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
p : I ⟶ Z
hZ : IsZero.{v, u} Z
obtain : Injective.{v, u} I ↔ MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
⊢ Injective.{v, u} I ↔ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p

Tactic:
obtain rfl := hZ.eq_of_tgt p 0

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt, OfNat.ofNat, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
mp : Injective.{v, u} I → MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
mpr : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0 → Injective.{v, u} I
⊢ Injective.{v, u} I ↔ MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : Injective.{v, u} I
A B : C
i : A ⟶ B
mp : Mono i → HasLiftingProperty (X := I) (Y := Z) i 0
⊢ MorphismProperty.monomorphisms C i → HasLiftingProperty (X := I) (Y := Z) i 0

Tactic:
(_ : Mono i)
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : Injective.{v, u} I
A B : C
i : A ⟶ B
h_1 : Mono i
⊢ HasLiftingProperty (X := I) (Y := Z) i 0

Tactic:
Injective.hasLiftingProperty_of_isZero i 0 hZ

Premises used: CategoryTheory.Injective.hasLiftingProperty_of_isZero, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : Injective.{v, u} I
A B : C
i : A ⟶ B
h_1 : Mono i
⊢ HasLiftingProperty (X := I) (Y := Z) i 0

Tactic:
exact Injective.hasLiftingProperty_of_isZero i 0 hZ

Premises used: CategoryTheory.Injective.hasLiftingProperty_of_isZero, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
mpr : ∀ {X Y : C} (g : X ⟶ I) (f : X ⟶ Y) [Mono f], ∃ (h : Y ⟶ I), f ≫ h = g
⊢ Injective.{v, u} I

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
⊢ HasLiftingProperty (X := I) (Y := Z) i 0

Tactic:
have := h _ hi
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty (X := I) (Y := Z) i 0
⊢ Eq (α := A ⟶ Z) (f ≫ 0) (i ≫ 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty (X := I) (Y := Z) i 0
⊢ CommSq (Z := Z) f i 0 0

Tactic:
have sq : CommSq f i (0 : I ⟶ Z) 0 := ⟨by simp⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty (X := I) (Y := Z) i 0
sq : CommSq (Z := Z) f i 0 0
⊢ i ≫ sq.lift = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty (X := I) (Y := Z) i 0
sq : CommSq (Z := Z) f i 0 0
⊢ ∃ (h : B ⟶ I), i ≫ h = f

Tactic:
exact ⟨sq.lift, by simp⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
I : C
⊢ Injective.{v, u} I ↔ MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0

Tactic:
injective_iff_rlp_monomorphisms_of_isZero _ (isZero_zero C)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.injective_iff_rlp_monomorphisms_of_isZero
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.PreservesInjectiveObjects
X : C
inst_4 : Injective.{v₁, u₁} X
⊢ Injective.{v₂, u₂} (F.obj X)

Tactic:
Functor.PreservesInjectiveObjects.injective_obj inferInstance

Premises used: CategoryTheory.Functor.PreservesInjectiveObjects.injective_obj, inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves
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 : F.PreservesInjectiveObjects
X : C
h : Injective.{v₁, u₁} X
⊢ Injective.{v₂, u₂} (F.obj X)

Tactic:
Functor.PreservesInjectiveObjects.injective_obj h

Premises used: CategoryTheory.Functor.PreservesInjectiveObjects.injective_obj