-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem infinite_pigeonhole_set {β α : Type u} {s : Set β} (f : s → α) (θ : Cardinal)
    (hθ : θ ≤ #s) (h₁ : ℵ₀ ≤ θ) (h₂ : #α < θ.ord.cof) :
    ∃ (a : α) (t : Set β) (h : t ⊆ s), θ ≤ #t ∧ ∀ ⦃x⦄ (hx : x ∈ t), f ⟨x, h hx⟩ = a

Proof state:
case intro.refine_1.intro
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
x : β
hx : x ∈ s
h✝ : f ⟨x, hx⟩ = a
⊢ x ∈ s

Tactic:
exact hx

Result:
no goals

Proof state:
case intro.refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ θ ≤ #↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}

Tactic:
refine
  ha.trans
    (ge_of_eq <|
      Quotient.sound ⟨Equiv.trans ?_ (Equiv.subtypeSubtypeEquivSubtypeExists _ _).symm⟩)

Result:
case intro.refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a} ≃ { a_1 // ∃ (h : a_1 ∈ s), ⟨a_1, h⟩ ∈ f ⁻¹' {a} }

Proof state:
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
⊢ ∃ a t, ∃ (h : t ⊆ s), θ ≤ #↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole_card f θ hθ h₁ h₂

Result:
case intro
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ∃ a t, ∃ (h : t ⊆ s), θ ≤ #↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a

Proof state:
case intro.refine_3.intro
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
x : β
w✝ : x ∈ s
hx' : f ⟨x, w✝⟩ = a
⊢ f ⟨x, ⋯⟩ = a

Tactic:
exact hx'

Result:
no goals

Proof state:
case intro
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ∃ a t, ∃ (h : t ⊆ s), θ ≤ #↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a

Tactic:
refine ⟨a, { x | ∃ h, f ⟨x, h⟩ = a }, ?_, ?_, ?_⟩

Result:
case intro.refine_1
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ {x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a} ⊆ s

case intro.refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ θ ≤ #↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}

case intro.refine_3
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ∀ ⦃x : β⦄ (hx : x ∈ {x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}), f ⟨x, ⋯⟩ = a

Proof state:
case intro.refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a} ≃ { a_1 // ∃ (h : a_1 ∈ s), ⟨a_1, h⟩ ∈ f ⁻¹' {a} }

Tactic:
simp only [coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_setOf_eq]

Result:
case intro.refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ { x // ∃ (h : x ∈ s), f ⟨x, h⟩ = a } ≃ { a_1 // ∃ (h : a_1 ∈ s), f ⟨a_1, ⋯⟩ = a }

Proof state:
case intro.refine_3
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ∀ ⦃x : β⦄ (hx : x ∈ {x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}), f ⟨x, ⋯⟩ = a

Tactic:
rintro x ⟨_, hx'⟩

Result:
case intro.refine_3.intro
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
x : β
w✝ : x ∈ s
hx' : f ⟨x, w✝⟩ = a
⊢ f ⟨x, ⋯⟩ = a

Proof state:
case intro.refine_1
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ {x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a} ⊆ s

Tactic:
rintro x ⟨hx, _⟩

Result:
case intro.refine_1.intro
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
x : β
hx : x ∈ s
h✝ : f ⟨x, hx⟩ = a
⊢ x ∈ s

Proof state:
case intro.refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ { x // ∃ (h : x ∈ s), f ⟨x, h⟩ = a } ≃ { a_1 // ∃ (h : a_1 ∈ s), f ⟨a_1, ⋯⟩ = a }

Tactic:
rfl

Result:
no goals