awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
inst_1 : Nonempty X
X_1 Y : Type u₁
g : X_1 ⟶ X
f : X_1 ⟶ Y
mono : Mono f
y : X_1
pos :
  ∀
    (h :
      Membership.mem (α := (fun (X : Type u₁) ↦ X) Y) (γ := Set ((fun (X : Type u₁) ↦ X) Y))
        (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
            (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
            y :
          (fun (X : Type u₁) ↦ X) Y)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
        (Classical.choose (p := fun (x : X_1) ↦
          Eq (α := (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                x :
              (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                y :
              (fun (X : Type u₁) ↦ X) Y))
          h) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
neg :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y) y :
        (fun (X : Type u₁) ↦ X) Y) ∉
      Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
          (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y) →
    Nonempty.some ⋯ = (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
⊢ (if h :
        Membership.mem (α := (fun (X : Type u₁) ↦ X) Y) (γ := Set ((fun (X : Type u₁) ↦ X) Y))
          (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
              (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
              y :
            (fun (X : Type u₁) ↦ X) Y) then
      (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
        (Classical.choose (p := fun (x : X_1) ↦
          Eq (α := (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                x :
              (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                y :
              (fun (X : Type u₁) ↦ X) Y))
          h)
    else Nonempty.some ⋯) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
inst_1 : Nonempty X
X_1 Y : Type u₁
g : X_1 ⟶ X
f : X_1 ⟶ Y
mono : Mono f
y : X_1
h :
  Membership.mem (α := (fun (X : Type u₁) ↦ X) Y) (γ := Set ((fun (X : Type u₁) ↦ X) Y))
    (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y) y :
      (fun (X : Type u₁) ↦ X) Y)
pos :
  ∀
    (mono :
      Function.Injective (α := (fun (X : Type u₁) ↦ X) X_1) (β := (fun (X : Type u₁) ↦ X) Y)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
    (y : X_1)
    (h :
      Membership.mem (α := (fun (X : Type u₁) ↦ X) Y) (γ := Set ((fun (X : Type u₁) ↦ X) Y))
        (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
            (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
            y :
          (fun (X : Type u₁) ↦ X) Y)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
        (Classical.choose (p := fun (x : X_1) ↦
          Eq (α := (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                x :
              (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                y :
              (fun (X : Type u₁) ↦ X) Y))
          h) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
      (Classical.choose (p := fun (x : X_1) ↦
        Eq (α := (fun (X : Type u₁) ↦ X) Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
              x :
            (fun (X : Type u₁) ↦ X) Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
              y :
            (fun (X : Type u₁) ↦ X) Y))
        h) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y

Tactic:
rw [mono_iff_injective] at mono

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
inst_1 : Nonempty X
X_1 Y : Type u₁
g : X_1 ⟶ X
f : X_1 ⟶ Y
mono :
  Function.Injective (α := (fun (X : Type u₁) ↦ X) X_1) (β := (fun (X : Type u₁) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
y : X_1
h :
  Membership.mem (α := (fun (X : Type u₁) ↦ X) Y) (γ := Set ((fun (X : Type u₁) ↦ X) Y))
    (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y) y :
      (fun (X : Type u₁) ↦ X) Y)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
      (Classical.choose (p := fun (x : X_1) ↦
        Eq (α := (fun (X : Type u₁) ↦ X) Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
              x :
            (fun (X : Type u₁) ↦ X) Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
              y :
            (fun (X : Type u₁) ↦ X) Y))
        h) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y

Tactic:
simp [mono (Classical.choose_spec h)]

Premises used: Classical.choose_spec
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
inst_1 : Nonempty X
X_1 Y : Type u₁
g : X_1 ⟶ X
f : X_1 ⟶ Y
mono : Mono f
y : X_1
h :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y) y :
      (fun (X : Type u₁) ↦ X) Y) ∉
    Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
⊢ Nonempty.some ⋯ = (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y

Tactic:
False.elim (h ⟨y, rfl⟩)

Premises used: False.elim, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
inst_1 : Nonempty X
X_1 Y : Type u₁
g : X_1 ⟶ X
f : X_1 ⟶ Y
mono : Mono f
y : X_1
h :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y) y :
      (fun (X : Type u₁) ↦ X) Y) ∉
    Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
⊢ Nonempty.some ⋯ = (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y

Tactic:
exact False.elim (h ⟨y, rfl⟩)

Premises used: False.elim, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
rw :
  Function.Injective (α := (fun (X : Type u₁) ↦ X) X) (β := (fun (X : Type u₁) ↦ X) (WithBot X))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾WithBot.some)) :
      (a : (fun (X : Type u₁) ↦ X) X) → (fun (X : Type u₁) ↦ X) (WithBot X))
⊢ Mono.{u₁, u₁ + 1} (X := X) (↾WithBot.some)

Tactic:
rw [mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
⊢ Function.Injective (α := (fun (X : Type u₁) ↦ X) X) (β := (fun (X : Type u₁) ↦ X) (WithBot X))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾WithBot.some)) :
      (a : (fun (X : Type u₁) ↦ X) X) → (fun (X : Type u₁) ↦ X) (WithBot X))

Tactic:
WithBot.coe_injective

Premises used: WithBot.some, WithBot.coe_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
⊢ Function.Injective (α := (fun (X : Type u₁) ↦ X) X) (β := (fun (X : Type u₁) ↦ X) (WithBot X))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾WithBot.some)) :
      (a : (fun (X : Type u₁) ↦ X) X) → (fun (X : Type u₁) ↦ X) (WithBot X))

Tactic:
exact WithBot.coe_injective

Premises used: WithBot.coe_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
h : f ≫ prod.lift (factorThru (g ≫ prod.fst) f) (factorThru (g ≫ prod.snd) f) = g
⊢ ∃ (h : Y ⟶ Limits.prod.{v₁, u₁} P Q), f ≫ h = g

Tactic:
use Limits.prod.lift (factorThru (g ≫ Limits.prod.fst) f) (factorThru (g ≫ Limits.prod.snd) f)

Premises used: CategoryTheory.Limits.prod.fst, CategoryTheory.Limits.prod.snd, CategoryTheory.CategoryStruct.comp, CategoryTheory.Injective.factorThru, CategoryTheory.Limits.prod.lift
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
h : prod.lift (g ≫ prod.fst) (g ≫ prod.snd) = g
⊢ f ≫ prod.lift (factorThru (g ≫ prod.fst) f) (factorThru (g ≫ prod.snd) f) = g

Tactic:
simp only [prod.comp_lift, comp_factorThru]

Premises used: CategoryTheory.Injective.comp_factorThru, CategoryTheory.Limits.prod.comp_lift
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
h :
  CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} P Q) (prod.lift (g ≫ prod.fst) (g ≫ prod.snd)) prod.fst = g ≫ prod.fst
h₁ :
  CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} P Q) (prod.lift (g ≫ prod.fst) (g ≫ prod.snd)) prod.snd = g ≫ prod.snd
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} P Q) (prod.lift (g ≫ prod.fst) (g ≫ prod.snd)) prod.fst = g ≫ prod.fst

Tactic:
simp only [prod.lift_fst]

Premises used: CategoryTheory.Limits.prod.lift_fst
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} P Q) (prod.lift (g ≫ prod.fst) (g ≫ prod.snd)) prod.snd = g ≫ prod.snd

Tactic:
simp only [prod.lift_snd]

Premises used: CategoryTheory.Limits.prod.lift_snd
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasProduct.{v, v₁, u₁} c
inst_2 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ piObj.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ piObj.{v, v₁, u₁} c), f ≫ h = g

Tactic:
⟨Pi.lift fun b => factorThru (g ≫ Pi.π c _) f, ?_⟩

Premises used: CategoryTheory.Limits.Pi.π, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Injective.factorThru, CategoryTheory.Limits.Pi.lift
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasProduct.{v, v₁, u₁} c
inst_2 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ piObj.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
refine : (f ≫ Pi.lift fun (b : β) ↦ factorThru (g ≫ Pi.π c b) f) = g
⊢ ∃ (h : Y ⟶ piObj.{v, v₁, u₁} c), f ≫ h = g

Tactic:
refine ⟨Pi.lift fun b => factorThru (g ≫ Pi.π c _) f, ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasProduct.{v, v₁, u₁} c
inst_2 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ piObj.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
h :
  ∀ (b : β),
    CategoryStruct.comp (Y := piObj.{v, v₁, u₁} c) (f ≫ Pi.lift fun (b : β) ↦ factorThru (g ≫ Pi.π c b) f) (Pi.π c b) =
      g ≫ Pi.π c b
⊢ (f ≫ Pi.lift fun (b : β) ↦ factorThru (g ≫ Pi.π c b) f) = g

Tactic:
ext b
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasProduct.{v, v₁, u₁} c
inst_2 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ piObj.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
b : β
⊢ CategoryStruct.comp (Y := piObj.{v, v₁, u₁} c) (f ≫ Pi.lift fun (b : β) ↦ factorThru (g ≫ Pi.π c b) f) (Pi.π c b) =
    g ≫ Pi.π c b

Tactic:
simp only [Category.assoc, limit.lift_π, Fan.mk_π_app, comp_factorThru]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Injective.comp_factorThru, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ biprod.{v₁, u₁} P Q), f ≫ h = g

Tactic:
⟨biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f), ?_⟩

Premises used: CategoryTheory.Limits.biprod.snd, CategoryTheory.Limits.biprod.lift, CategoryTheory.Limits.biprod.fst, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Injective.factorThru
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
refine : f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f) = g
⊢ ∃ (h : Y ⟶ biprod.{v₁, u₁} P Q), f ≫ h = g

Tactic:
refine ⟨biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f), ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
h₀ :
  CategoryStruct.comp (Y := biprod.{v₁, u₁} P Q)
      (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) biprod.fst =
    g ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v₁, u₁} P Q)
      (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) biprod.snd =
    g ≫ biprod.snd
⊢ f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f) = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ CategoryStruct.comp (Y := biprod.{v₁, u₁} P Q)
      (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) biprod.fst =
    g ≫ biprod.fst

Tactic:
simp only [Category.assoc, biprod.lift_fst, comp_factorThru]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_fst, CategoryTheory.Injective.comp_factorThru
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ CategoryStruct.comp (Y := biprod.{v₁, u₁} P Q)
      (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) biprod.snd =
    g ≫ biprod.snd

Tactic:
simp only [Category.assoc, biprod.lift_snd, comp_factorThru]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_snd, CategoryTheory.Injective.comp_factorThru
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBiproduct.{v, v₁, u₁} c
inst_3 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ biproduct.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ biproduct.{v, v₁, u₁} c), f ≫ h = g

Tactic:
⟨biproduct.lift fun b => factorThru (g ≫ biproduct.π _ _) f, ?_⟩

Premises used: CategoryTheory.Limits.biproduct.lift, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Injective.factorThru, CategoryTheory.Limits.biproduct.π
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBiproduct.{v, v₁, u₁} c
inst_3 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ biproduct.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
refine : (f ≫ biproduct.lift fun (b : β) ↦ factorThru (g ≫ biproduct.π c b) f) = g
⊢ ∃ (h : Y ⟶ biproduct.{v, v₁, u₁} c), f ≫ h = g

Tactic:
refine ⟨biproduct.lift fun b => factorThru (g ≫ biproduct.π _ _) f, ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBiproduct.{v, v₁, u₁} c
inst_3 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ biproduct.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
w :
  ∀ (j : β),
    CategoryStruct.comp (Y := biproduct.{v, v₁, u₁} c)
        (f ≫ biproduct.lift fun (b : β) ↦ factorThru (g ≫ biproduct.π c b) f) (biproduct.π c j) =
      g ≫ biproduct.π c j
⊢ (f ≫ biproduct.lift fun (b : β) ↦ factorThru (g ≫ biproduct.π c b) f) = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBiproduct.{v, v₁, u₁} c
inst_3 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ biproduct.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
j : β
⊢ CategoryStruct.comp (Y := biproduct.{v, v₁, u₁} c)
      (f ≫ biproduct.lift fun (b : β) ↦ factorThru (g ≫ biproduct.π c b) f) (biproduct.π c j) =
    g ≫ biproduct.π c j

Tactic:
simp only [Category.assoc, biproduct.lift_π, comp_factorThru]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Injective.comp_factorThru, CategoryTheory.Limits.biproduct.lift_π
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Cᵒᵖ
inst_1 : Projective.{v₁, u₁} P
X Y : C
g : X ⟶ unop P
f : X ⟶ Y
mono : Mono f
⊢ Quiver.Hom.op (f ≫ Quiver.Hom.unop (Projective.factorThru g.op f.op)) = g.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Cᵒᵖ
inst_1 : Injective.{v₁, u₁} J
E X : C
f : unop J ⟶ X
e : E ⟶ X
he : Epi e
⊢ Quiver.Hom.op (Quiver.Hom.unop (factorThru f.op e.op) ≫ e) = f.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : C
inst_1 : Injective.{v₁, u₁} J
E X : Cᵒᵖ
f : op J ⟶ X
e : E ⟶ X
epi : Epi e
⊢ Quiver.Hom.unop ((factorThru f.unop e.unop).op ≫ e) = f.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : C
inst_1 : Projective.{v₁, u₁} P
X Y : Cᵒᵖ
g : X ⟶ op P
f : X ⟶ Y
mono : Mono f
⊢ (f ≫ (Projective.factorThru g.unop f.unop).op).unop = g.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : C
⊢ Injective.{v₁, u₁} J ↔ Projective.{v₁, u₁} (op J)

Tactic:
⟨fun _ => inferInstance, fun _ => show Injective (unop (op J)) from inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : C
⊢ Projective.{v₁, u₁} P ↔ Injective.{v₁, u₁} (op P)

Tactic:
⟨fun _ => inferInstance, fun _ => show Projective (unop (op P)) from inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : C
rw :
  Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op (op J))) ↔
    Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda J)
⊢ Injective.{v₁, u₁} J ↔ Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda J)

Tactic:
rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]

Premises used: CategoryTheory.Injective.injective_iff_projective_op, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : C
⊢ Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op (op J))) ↔
    Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda J)

Tactic:
Functor.preservesEpimorphisms.iso_iff (Coyoneda.objOpOp _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms.iso_iff, CategoryTheory.Coyoneda.objOpOp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : C
⊢ Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op (op J))) ↔
    Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda J)

Tactic:
exact Functor.preservesEpimorphisms.iso_iff (Coyoneda.objOpOp _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms.iso_iff, CategoryTheory.Coyoneda.objOpOp