-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem eventually_injective [Nonempty J] [Finite F.sections] :
    ∃ j, ∀ (i) (f : i ⟶ j), (F.map f).Injective

Proof state:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Tactic:
let fn j := Fintype.card F.sections - Fintype.card (F.obj j)

Result:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Proof state:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Tactic:
have card_le : ∀ j, Fintype.card (F.obj j) ≤ Fintype.card F.sections :=
  fun j => Fintype.card_le_of_surjective _ (F.eval_section_surjective_of_surjective Fsur j)

Result:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Proof state:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)
i : J
f : i ⟶ Function.argmin fn
⊢ Fintype.card (F.obj i) ≤ Fintype.card (F.obj (Function.argmin fn))

Tactic:
rw [← Nat.sub_le_sub_iff_left (card_le i)]

Result:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)
i : J
f : i ⟶ Function.argmin fn
⊢ Fintype.card ↑F.sections - Fintype.card (F.obj (Function.argmin fn)) ≤
    Fintype.card ↑F.sections - Fintype.card (F.obj i)

Proof state:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Tactic:
haveI : ∀ j, Fintype (F.obj j) := fun j => Fintype.ofFinite (F.obj j)

Result:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this : (j : J) → Fintype (F.obj j)
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Proof state:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this : (j : J) → Fintype (F.obj j)
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Tactic:
haveI : Fintype F.sections := Fintype.ofFinite F.sections

Result:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Proof state:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)
i : J
f : i ⟶ Function.argmin fn
⊢ Fintype.card ↑F.sections - Fintype.card (F.obj (Function.argmin fn)) ≤
    Fintype.card ↑F.sections - Fintype.card (F.obj i)

Tactic:
apply fn.argmin_le

Result:
no goals

Proof state:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)

Tactic:
refine ⟨fn.argmin,
  fun i f => ((Fintype.bijective_iff_surjective_and_card _).2
    ⟨Fsur f, le_antisymm ?_ (Fintype.card_le_of_surjective _ <| Fsur f)⟩).1⟩

Result:
J : Type u
inst✝⁵ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)
i : J
f : i ⟶ Function.argmin fn
⊢ Fintype.card (F.obj i) ≤ Fintype.card (F.obj (Function.argmin fn))