α✝ : Type ?u.148026
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
w : (#α) < (#β)
w' : ℵ₀ ≤ (#α)
⊢ ∃ a, succ (#α) ≤ (#↑(f ⁻¹' {a}))
α✝ : Type ?u.148026
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
w : (#α) < (#β)
w' : ℵ₀ ≤ (#α)
⊢ ∃ a, (#α) < (#↑(f ⁻¹' {a}))
simp_rw [← succ_le_iff]
no goals
α✝ : Type ?u.148026
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
w : (#α) < (#β)
w' : ℵ₀ ≤ (#α)
⊢ ∃ a, succ (#α) ≤ (#↑(f ⁻¹' {a}))
exact
  Ordinal.infinite_pigeonhole_card f (succ (#α)) (succ_le_of_lt w) (w'.trans (lt_succ _).le)
    ((lt_succ _).trans_le (isRegular_succ w').2.ge)