case intro
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ ∃ a t h, θ ≤ (#↑t) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f { val := x, property := (_ : x ∈ s) } = a
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
⊢ ∃ a t h, θ ≤ (#↑t) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f { val := x, property := (_ : x ∈ s) } = a
cases' infinite_pigeonhole_card f θ hθ h₁ h₂ with a ha
case intro.refine'_1
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ {x | ∃ h, f { val := x, property := h } = a} ⊆ s

case intro.refine'_2
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ θ ≤ (#↑{x | ∃ h, f { val := x, property := h } = a})

case intro.refine'_3
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ ∀ ⦃x : β⦄ (hx : x ∈ {x | ∃ h, f { val := x, property := h } = a}), f { val := x, property := (_ : x ∈ s) } = a
case intro
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ ∃ a t h, θ ≤ (#↑t) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f { val := x, property := (_ : x ∈ s) } = a
refine' ⟨a, { x | ∃ h, f ⟨x, h⟩ = a }, _, _, _⟩
case intro.refine'_3.intro
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
x : β
w✝ : x ∈ s
hx' : f { val := x, property := w✝ } = a
⊢ f { val := x, property := (_ : x ∈ s) } = a
case intro.refine'_3
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ ∀ ⦃x : β⦄ (hx : x ∈ {x | ∃ h, f { val := x, property := h } = a}), f { val := x, property := (_ : x ∈ s) } = a
rintro x ⟨_, hx'⟩
no goals
case intro.refine'_3.intro
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
x : β
w✝ : x ∈ s
hx' : f { val := x, property := w✝ } = a
⊢ f { val := x, property := (_ : x ∈ s) } = a
exact hx'
case intro.refine'_1.intro
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
x : β
hx : x ∈ s
h✝ : f { val := x, property := hx } = a
⊢ x ∈ s
case intro.refine'_1
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ {x | ∃ h, f { val := x, property := h } = a} ⊆ s
rintro x ⟨hx, _⟩
no goals
case intro.refine'_1.intro
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
x : β
hx : x ∈ s
h✝ : f { val := x, property := hx } = a
⊢ x ∈ s
exact hx
case intro.refine'_2
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ ↑{x | ∃ h, f { val := x, property := h } = a} ≃ { a_1 // ∃ h, { val := a_1, property := h } ∈ f ⁻¹' {a} }
case intro.refine'_2
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ θ ≤ (#↑{x | ∃ h, f { val := x, property := h } = a})
refine'
  ha.trans
    (ge_of_eq <|
      Quotient.sound ⟨Equiv.trans _ (Equiv.subtypeSubtypeEquivSubtypeExists _ _).symm⟩)
case intro.refine'_2
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ { x // ∃ h, f { val := x, property := h } = a } ≃ { a_1 // ∃ h, f { val := a_1, property := (_ : a_1 ∈ s) } = a }
case intro.refine'_2
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ ↑{x | ∃ h, f { val := x, property := h } = a} ≃ { a_1 // ∃ h, { val := a_1, property := h } ∈ f ⁻¹' {a} }
simp only [coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_setOf_eq]
no goals
case intro.refine'_2
α✝ : Type ?u.111380
r : α✝ → α✝ → Prop
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal
hθ : θ ≤ (#↑s)
h₁ : ℵ₀ ≤ θ
h₂ : (#α) < cof (ord θ)
a : α
ha : θ ≤ (#↑(f ⁻¹' {a}))
⊢ { x // ∃ h, f { val := x, property := h } = a } ≃ { a_1 // ∃ h, f { val := a_1, property := (_ : a_1 ∈ s) } = a }
rfl