awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
refine : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a

Tactic:
refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
h : Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
⊢ (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)

Tactic:
apply Nonempty.some

Premises used: Nonempty.some
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
h : Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
⊢ Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))

Tactic:
apply Cardinal.eq.1

Premises used: Cardinal.eq, Iff.mp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
h : ∀ (val : Fintype α), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
⊢ Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
h : ∀ (val : Fintype β), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
⊢ Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
h : Fintype.card (↑(f ⁻¹' {c}) : Type) = Fintype.card (↑(g ⁻¹' {c}) : Type)
⊢ Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)

Tactic:
simp only [Cardinal.mk_fintype, Nat.cast_inj]

Premises used: Nat.cast_inj, Cardinal.mk_fintype
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
rw :
  Eq.{max 1 (v + 1)} (α := Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
    (((o.matrixDecomposition :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
              ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
          (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
            (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
        (i.hom ≫ i.inv) c :
      Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
    (1 : Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
⊢ HMul.hMul (α := Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c))) (β :=
      Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                  (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
                ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
              (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
          i.inv c :
        Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                  (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
                ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
              (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
          i.hom c :
        Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c))) =
    1

Tactic:
rw [← o.matrixDecomposition_comp]

Premises used: CategoryTheory.HomOrthogonal.matrixDecomposition_comp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
⊢ Eq.{max 1 (v + 1)} (α := Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
    (((o.matrixDecomposition :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
              ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
          (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
            (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
        (i.hom ≫ i.inv) c :
      Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
    (1 : Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
rw :
  Eq.{max 1 (v + 1)} (α := Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
    (((o.matrixDecomposition :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
              ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
          (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
            (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
        (i.inv ≫ i.hom) c :
      Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
    (1 : Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
⊢ HMul.hMul (α := Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c))) (β :=
      Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                  (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
                ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
              (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
          i.hom c :
        Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                  (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
                ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
              (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
          i.inv c :
        Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c))) =
    1

Tactic:
rw [← o.matrixDecomposition_comp]

Premises used: CategoryTheory.HomOrthogonal.matrixDecomposition_comp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
⊢ Eq.{max 1 (v + 1)} (α := Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
    (((o.matrixDecomposition :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
              ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
          (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
            (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
        (i.inv ≫ i.hom) c :
      Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
    (1 : Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
⊢ Fintype.card (↑(f ⁻¹' {c}) : Type) = Fintype.card (↑(g ⁻¹' {c}) : Type)

Tactic:
exact
    Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)

Premises used: CategoryTheory.HomOrthogonal.matrixDecomposition, Matrix.square_of_invertible, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
refine refine₁ : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
h : ∀ (c : ι), Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
h₁ : ∀ (c : ι), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
h₂ h₃ : ∀ (c : ι) (val : Fintype α), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
h₄ :
  ∀ (c : ι) (val : Fintype α) (val : Fintype β), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
h₅ :
  ∀ (c : ι) (val : Fintype α) (val_1 : Fintype β),
    Fintype.card (↑(f ⁻¹' {c}) : Type) = Fintype.card (↑(g ⁻¹' {c}) : Type)
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a

Tactic:
classical
  refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
  intro c
  apply Nonempty.some
  apply Cardinal.eq.1
  cases nonempty_fintype α; cases nonempty_fintype β
  simp only [Cardinal.mk_fintype, Nat.cast_inj]
  exact
    Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)

Premises used: Nonempty.some, Nat.cast_inj, Cardinal.mk_fintype, nonempty_fintype, Cardinal.eq, Iff.mp
-- Module: Mathlib.CategoryTheory.Preadditive.Indization
Goal:
C : Type u
inst : SmallCategory C
inst_1 : Preadditive C
inst_2 : HasFiniteColimits C
⊢ HasFiniteBiproducts.{u, u + 1} (Ind C)

Tactic:
HasFiniteBiproducts.of_hasFiniteCoproducts

Premises used: CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J X Y : C
inst_1 : Injective.{v₁, u₁} J
g : X ⟶ J
f : X ⟶ Y
inst_2 : Mono f
⊢ f ≫ factorThru g f = g

Tactic:
(Injective.factors g f).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.Injective.factorThru, CategoryTheory.Injective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
⊢ Injective.{v₁, u₁} (C := C) 0

Tactic:
(isZero_zero C).injective

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
obtain : ∀ (h : Y ⟶ P) (h_eq : f ≫ h = g ≫ i.inv), ∃ (h : Y ⟶ Q), f ≫ h = g
⊢ ∃ (h : Y ⟶ Q), f ≫ h = g

Tactic:
obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv, CategoryTheory.Injective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ (h : Y ⟶ Q), f ≫ h = g

Tactic:
⟨h ≫ i.hom, ?_⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
refine : f ≫ h ≫ i.hom = g
⊢ ∃ (h : Y ⟶ Q), f ≫ h = g

Tactic:
refine ⟨h ≫ i.hom, ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
rw : (f ≫ h) ≫ i.hom = g
rw₁ : (g ≫ i.inv) ≫ i.hom = g
rw₂ : g ≫ i.inv ≫ i.hom = g
rw₃ : g ≫ 𝟙 Q = g
rw₄ rw₅ : g = g
⊢ f ≫ h ≫ i.hom = g

Tactic:
rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
⊢ Injective.{v₁, u₁} P ↔ Injective.{v₁, u₁} Q

Tactic:
⟨of_iso i, of_iso i.symm⟩

Premises used: CategoryTheory.Injective.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- 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
z : Y
⊢ X

Tactic:
exact
          if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some inferInstance

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, Nonempty.some, Set.range, DFunLike.coe
-- 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
z : Y
⊢ X

Tactic:
classical
      exact
          if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some inferInstance

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, Nonempty.some, Set.range, DFunLike.coe
-- 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
h :
  ∀ (y : X_1),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f ≫
            ↾fun (z : Y) ↦
              if h :
                  Membership.mem (γ := 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))
                    z 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) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f :
                          (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                        x =
                      z)
                    h)
              else Nonempty.some ⋯))
        y =
      (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
⊢ (f ≫
      ↾fun (z : Y) ↦
        if h :
            Membership.mem (γ := 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))
              z 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) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                  x =
                z)
              h)
        else Nonempty.some ⋯) =
    g

Tactic:
ext y
-- 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 :
  (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
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f ≫
          ↾fun (z : Y) ↦
            if h :
                Membership.mem (γ := 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))
                  z 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) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f :
                        (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                      x =
                    z)
                  h)
            else Nonempty.some ⋯))
      y =
    (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y

Tactic:
change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, Membership.mem, dite, Classical.choose, Set.range, DFunLike.coe