-- Mathlib/CategoryTheory/Comma/CardinalArrow.lean
lemma Arrow.finite_iff (C : Type u) [SmallCategory C] :
    Finite (Arrow C) ↔ Nonempty (FinCategory C)

Proof state:
case mp.refine_2
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
⊢ Fintype (a ⟶ b)

Tactic:
have := Finite.of_injective (fun (f : a ⟶ b) ↦ Arrow.mk f)
  (fun f g h ↦ by
    change (Arrow.mk f).hom = (Arrow.mk g).hom
    congr)

Result:
case mp.refine_2
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
this : Finite (a ⟶ b)
⊢ Fintype (a ⟶ b)

Proof state:
case mp.refine_2
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
this : Finite (a ⟶ b)
⊢ Fintype (a ⟶ b)

Tactic:
apply Fintype.ofFinite

Result:
no goals

Proof state:
C : Type u
inst✝ : SmallCategory C
⊢ Finite (Arrow C) ↔ Nonempty (FinCategory C)

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : SmallCategory C
⊢ Finite (Arrow C) → Nonempty (FinCategory C)

case mpr
C : Type u
inst✝ : SmallCategory C
⊢ Nonempty (FinCategory C) → Finite (Arrow C)

Proof state:
case mpr.intro
C : Type u
inst✝ : SmallCategory C
val✝ : FinCategory C
this : Fintype (Arrow C)
⊢ Finite (Arrow C)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
f g : a ⟶ b
h : (fun f => mk f) f = (fun f => mk f) g
⊢ f = g

Tactic:
change (Arrow.mk f).hom = (Arrow.mk g).hom

Result:
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
f g : a ⟶ b
h : (fun f => mk f) f = (fun f => mk f) g
⊢ (mk f).hom = (mk g).hom

Proof state:
case mp.refine_1
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
this : Finite C
⊢ Fintype C

Tactic:
apply Fintype.ofFinite

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Nonempty (FinCategory C)

Tactic:
refine ⟨?_, fun a b ↦ ?_⟩

Result:
case mp.refine_1
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Fintype C

case mp.refine_2
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
⊢ Fintype (a ⟶ b)

Proof state:
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
f g : a ⟶ b
h : (fun f => mk f) f = (fun f => mk f) g
⊢ (mk f).hom = (mk g).hom

Tactic:
congr

Result:
no goals

Proof state:
case mp.refine_1
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Fintype C

Tactic:
have := Finite.of_injective (fun (a : C) ↦ Arrow.mk (𝟙 a))
  (fun _ _  ↦ congr_arg Comma.left)

Result:
case mp.refine_1
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
this : Finite C
⊢ Fintype C

Proof state:
case mpr.intro
C : Type u
inst✝ : SmallCategory C
val✝ : FinCategory C
⊢ Finite (Arrow C)

Tactic:
have := Fintype.ofEquiv  _ (Arrow.equivSigma C).symm

Result:
case mpr.intro
C : Type u
inst✝ : SmallCategory C
val✝ : FinCategory C
this : Fintype (Arrow C)
⊢ Finite (Arrow C)

Proof state:
case mp
C : Type u
inst✝ : SmallCategory C
⊢ Finite (Arrow C) → Nonempty (FinCategory C)

Tactic:
intro

Result:
case mp
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Nonempty (FinCategory C)

Proof state:
case mpr
C : Type u
inst✝ : SmallCategory C
⊢ Nonempty (FinCategory C) → Finite (Arrow C)

Tactic:
rintro ⟨_⟩

Result:
case mpr.intro
C : Type u
inst✝ : SmallCategory C
val✝ : FinCategory C
⊢ Finite (Arrow C)