α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ Set.range f = Set.range ↑(orderEmbOfFin s h)
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ f = ↑(orderEmbOfFin s h)
apply Fin.strictMono_unique hmono (s.orderEmbOfFin h).strictMono
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ Set.range f = Set.range ↑(orderEmbOfFin s h)
rw [range_orderEmbOfFin, ← Set.image_univ, ← coe_univ, ← coe_image, coe_inj]
case refine'_1
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s

case refine'_2
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ card s ≤ card (image f univ)
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s
refine' eq_of_subset_of_card_le (fun x hx => _) _
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left✝ : x ∈ univ
hx : f x ∈ image f univ
⊢ f x ∈ s
case refine'_1
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s
rcases mem_image.1 hx with ⟨x, _, rfl⟩
no goals
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left✝ : x ∈ univ
hx : f x ∈ image f univ
⊢ f x ∈ s
exact hfs x
no goals
case refine'_2
α : Type u_1
β : Type ?u.51338
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ card s ≤ card (image f univ)
rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]