case intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
⊢ ∃ a, (#↑s) ≤ (#↑(f ⁻¹' {a}))
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
θ : Cardinal
hθ : θ ≤ (#β)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
⊢ ∃ a, θ ≤ (#↑(f ⁻¹' {a}))
rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩
case intro.intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
a : α
ha : (#↑(f ∘ Subtype.val ⁻¹' {a})) = (#↑s)
⊢ ∃ a, (#↑s) ≤ (#↑(f ⁻¹' {a}))
case intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
⊢ ∃ a, (#↑s) ≤ (#↑(f ⁻¹' {a}))
cases' infinite_pigeonhole (f ∘ Subtype.val : s → α) h₁ h₂ with a ha
case intro.intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
a : α
ha : (#↑(f ∘ Subtype.val ⁻¹' {a})) = (#↑s)
⊢ (#↑s) ≤ (#↑(f ⁻¹' {a}))
case intro.intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
a : α
ha : (#↑(f ∘ Subtype.val ⁻¹' {a})) = (#↑s)
⊢ ∃ a, (#↑s) ≤ (#↑(f ⁻¹' {a}))
use a
case intro.intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
a : α
ha : (#↑(f ∘ Subtype.val ⁻¹' {a})) = (#↑s)
⊢ (#↑(Subtype.val ⁻¹' (f ⁻¹' {a}))) ≤ (#↑(f ⁻¹' {a}))
case intro.intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
a : α
ha : (#↑(f ∘ Subtype.val ⁻¹' {a})) = (#↑s)
⊢ (#↑s) ≤ (#↑(f ⁻¹' {a}))
rw [← ha, @preimage_comp _ _ _ Subtype.val f]
no goals
case intro.intro
α✝ : Type ?u.110625
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
s : Set β
hθ : (#↑s) ≤ (#β)
h₁ : ℵ₀ ≤ (#↑s)
h₂ : (#α) < cof (ord (#↑s))
a : α
ha : (#↑(f ∘ Subtype.val ⁻¹' {a})) = (#↑s)
⊢ (#↑(Subtype.val ⁻¹' (f ⁻¹' {a}))) ≤ (#↑(f ⁻¹' {a}))
exact mk_preimage_of_injective _ _ Subtype.val_injective