awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
rw : ∀ (ha : a.card < c) (hb : b.card < c), a.card + b.card < c
⊢ (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) a b < c.ord

Tactic:
rw [lt_ord, card_add] at *

Premises used: Ordinal.card_add, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c

Tactic:
add_lt_of_lt hc ha hb

Premises used: Cardinal.add_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c

Tactic:
exact add_lt_of_lt hc ha hb

Premises used: Cardinal.add_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
rw : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) o.card.ord
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) o

Tactic:
rw [← h.ord_card]

Premises used: Ordinal.IsInitial.ord_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
hc : ℵ₀ ≤ o.card
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) o.card.ord

Tactic:
apply isPrincipal_add_ord

Premises used: Ordinal.isPrincipal_add_ord
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho hc hc₁ hc₂ hc₃ : ω ≤ o
⊢ ℵ₀ ≤ o.card

Tactic:
rwa [aleph0_le_card]

Premises used: Ordinal.aleph0_le_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)

Tactic:
(isInitial_omega o).isPrincipal_add (omega0_le_omega o)

Premises used: Ordinal.omega0_le_omega, Ordinal.isInitial_omega, Ordinal.IsInitial.isPrincipal_add
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
rw : ∀ (ha : a.card < c) (hb : b.card < c), a.card * b.card < c
⊢ (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) a b < c.ord

Tactic:
rw [lt_ord, card_mul] at *

Premises used: Ordinal.card_mul, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card * b.card < c

Tactic:
mul_lt_of_lt hc ha hb

Premises used: Cardinal.mul_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card * b.card < c

Tactic:
exact mul_lt_of_lt hc ha hb

Premises used: Cardinal.mul_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
rw : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) o.card.ord
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) o

Tactic:
rw [← h.ord_card]

Premises used: Ordinal.IsInitial.ord_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
hc : ℵ₀ ≤ o.card
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) o.card.ord

Tactic:
apply isPrincipal_mul_ord

Premises used: Ordinal.isPrincipal_mul_ord
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)

Tactic:
(isInitial_omega o).isPrincipal_mul (omega0_le_omega o)

Premises used: Ordinal.IsInitial.isPrincipal_mul, Ordinal.omega0_le_omega, Ordinal.isInitial_omega
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
by_contra! : ∀ (h : ∀ (a : α), #(↑(f ⁻¹' {a}) : Type u) < #β), False
⊢ ∃ (a : α), #β ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
by_contra! h
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #(↑(f ⁻¹' {a}) : Type u) < #β
apply : #(↑Set.univ : Type u) < #β
apply₁ : Type u
⊢ False

Tactic:
apply mk_univ.not_lt

Premises used: Cardinal.mk_univ, Eq.not_lt
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #(↑(f ⁻¹' {a}) : Type u) < #β
⊢ #(↑(⋃ (i : α), f ⁻¹' {i}) : Type u) < #β

Tactic:
mk_iUnion_le_sum_mk.trans_lt <| (sum_le_mk_mul_iSup _).trans_lt <|
        mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt_of_lt_cof_ord h₂ h)

Premises used: Cardinal.iSup_lt_of_lt_cof_ord, Cardinal.sum_le_mk_mul_iSup, Cardinal.mk_iUnion_le_sum_mk, Cardinal.mul_lt_of_lt, LT.lt.trans_le, Ordinal.cof_ord_le, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
⊢ ∃ (a : α), #β ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
have : ∃ a, #β ≤ #(f ⁻¹' {a}) := by
    by_contra! h
    apply mk_univ.not_lt
    rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]
    exact
      mk_iUnion_le_sum_mk.trans_lt <| (sum_le_mk_mul_iSup _).trans_lt <|
        mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt_of_lt_cof_ord h₂ h)
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
this : ∃ (a : α), #β ≤ #(↑(f ⁻¹' {a}) : Type u)
obtain : ∀ (x : α) (h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)), ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β
⊢ ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β

Tactic:
obtain ⟨x, h⟩ := this
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)
⊢ ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β

Tactic:
⟨x, h.antisymm' ?_⟩

Premises used: LE.le.antisymm', Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)
refine : #(↑(f ⁻¹' {x}) : Type u) ≤ #β
⊢ ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β

Tactic:
refine ⟨x, h.antisymm' ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)
rw : ∃ (p : Set β), #(↑p : Type u) = #(↑(f ⁻¹' {x}) : Type u)
⊢ #(↑(f ⁻¹' {x}) : Type u) ≤ #β

Tactic:
rw [le_mk_iff_exists_set]

Premises used: Cardinal.le_mk_iff_exists_set
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)
⊢ ∃ (p : Set β), #(↑p : Type u) = #(↑(f ⁻¹' {x}) : Type u)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)
⊢ ∃ (p : Set β), #(↑p : Type u) = #(↑(f ⁻¹' {x}) : Type u)

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
θ : Cardinal.{u}
hθ : θ ≤ #β
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
rcases :
  ∀ (s : Set β) (hθ : #(↑s : Type u) ≤ #β) (h₁ : ℵ₀ ≤ #(↑s : Type u)) (h₂ : #α < (#(↑s : Type u)).ord.cof),
    ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), θ ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩

Premises used: Cardinal.le_mk_iff_exists_set, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
obtain :
  ∀ (a : α) (ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)),
    ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole (f ∘ Subtype.val : s → α) h₁ h₂

Premises used: Cardinal.infinite_pigeonhole, Function.comp, Subtype.val
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
a : α
ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)
h : #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
use a
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
a : α
ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)
h : #(↑(Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' f ⁻¹' {a}) : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
rw [← ha, @preimage_comp _ _ _ Subtype.val f]

Premises used: Set.preimage_comp
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
a : α
ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)
⊢ #(↑(Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' f ⁻¹' {a}) : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
mk_preimage_of_injective _ _ Subtype.val_injective

Premises used: Subtype.val_injective, Cardinal.mk_preimage_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
a : α
ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)
⊢ #(↑(Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' f ⁻¹' {a}) : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
exact mk_preimage_of_injective _ _ Subtype.val_injective

Premises used: Subtype.val_injective, Cardinal.mk_preimage_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
obtain :
  ∀ (a : α) (ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)),
    ∃ (a : α) (t : Set β) (h : t ⊆ s),
      θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a
⊢ ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a

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

Premises used: Cardinal.infinite_pigeonhole_card
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a

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

Premises used: setOf, Exists, Subtype.mk, And.intro, Exists.intro, Eq
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
refine_1 : {x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} ⊆ s
refine_2 : θ ≤ #(↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u)
refine_3 :
  ∀ ⦃x : β⦄
    (hx : Membership.mem (γ := Set β) {x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} x),
    f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a
⊢ ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a

Tactic:
refine ⟨a, { x | ∃ h, f ⟨x, h⟩ = a }, ?_, ?_, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
x : β
hx : x ∈ s
h : f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x hx) = a
⊢ x ∈ s

Tactic:
hx
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
x : β
hx : x ∈ s
h : f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x hx) = a
⊢ x ∈ s

Tactic:
exact hx
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ θ ≤ #(↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u)

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

Premises used: Equiv.trans, ge_of_eq, Nonempty.intro, Equiv.subtypeSubtypeEquivSubtypeExists, LE.le.trans, Quotient.sound, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
refine_2 :
  (↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u) ≃
    { a_1 : β // ∃ (h : a_1 ∈ s), Subtype.mk (p := fun (x : β) ↦ x ∈ s) a_1 h ∈ f ⁻¹' {a} }
⊢ θ ≤ #(↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u)

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

Premises used: Equiv.trans, ge_of_eq, Nonempty.intro, Equiv.subtypeSubtypeEquivSubtypeExists, LE.le.trans, Quotient.sound, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ { x : β // ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a } ≃
    { x : β // ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a }

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
x : β
w : x ∈ s
hx' : f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x w) = a
⊢ f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a

Tactic:
hx'
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
x : β
w : x ∈ s
hx' : f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x w) = a
⊢ f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a

Tactic:
exact hx'
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
simp_rw : ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), #α < #(↑(f ⁻¹' {a}) : Type u)

Tactic:
simp_rw [← succ_le_iff]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
inr : ∀ (hα : ℵ₀ ≤ #α), ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
rcases lt_or_ge #α ℵ₀ with hα | hα

Premises used: Cardinal.mk, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
rwa rwa₁ rwa₂ rwa₃ : #α < ℵ₀
⊢ #α < ℵ₀.ord.cof

Tactic:
rwa [isRegular_aleph0.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord, Cardinal.isRegular_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
inl : ∀ (a : α) (ha : ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)), ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole_card f ℵ₀ hβ le_rfl
      (by rwa [isRegular_aleph0.cof_ord])

Premises used: le_rfl, Cardinal.infinite_pigeonhole_card, Cardinal.aleph0
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
a : α
ha : ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
⟨a, ha.trans' (succ_le_of_lt hα)⟩

Premises used: Order.succ_le_of_lt, Exists.intro, LE.le.trans'
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
a : α
ha : ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
exact ⟨a, ha.trans' (succ_le_of_lt hα)⟩
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : ℵ₀ ≤ #α
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
infinite_pigeonhole_card f (succ #α) (succ_le_of_lt h) (hα.trans (le_succ _))
      ((lt_succ _).trans_le (isRegular_succ hα).2.ge)

Premises used: Order.succ, LE.le.ge, Cardinal.mk, Order.succ_le_of_lt, Cardinal.infinite_pigeonhole_card, Cardinal.isRegular_succ, Order.lt_succ, LT.lt.trans_le, Order.le_succ, LE.le.trans, Cardinal.IsRegular.le_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : ℵ₀ ≤ #α
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
exact infinite_pigeonhole_card f (succ #α) (succ_le_of_lt h) (hα.trans (le_succ _))
      ((lt_succ _).trans_le (isRegular_succ hα).2.ge)

Premises used: Order.succ, LE.le.ge, Cardinal.mk, Order.succ_le_of_lt, Cardinal.infinite_pigeonhole_card, Cardinal.isRegular_succ, Order.lt_succ, LT.lt.trans_le, Order.le_succ, LE.le.trans, Cardinal.IsRegular.le_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
simp_rw : ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), Infinite.{u + 1} (↑(f ⁻¹' {a}) : Type u)

Tactic:
simp_rw [Cardinal.infinite_iff]

Premises used: Cardinal.infinite_iff
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
inr : ∀ (hα : ℵ₀ ≤ #α), ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
rcases lt_or_ge #α ℵ₀ with hα | hα

Premises used: Cardinal.mk, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
hα : #α < ℵ₀
rwa rwa₁ rwa₂ rwa₃ : #α < ℵ₀
⊢ #α < ℵ₀.ord.cof

Tactic:
rwa [isRegular_aleph0.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord, Cardinal.isRegular_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
hα : #α < ℵ₀
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
exact infinite_pigeonhole_card f ℵ₀ (aleph0_le_mk β) le_rfl
      (by rwa [isRegular_aleph0.cof_ord])

Premises used: le_rfl, Cardinal.infinite_pigeonhole_card, Cardinal.aleph0, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
hα : ℵ₀ ≤ #α
inr : ∀ (a : α) (ha : #α < #(↑(f ⁻¹' {a}) : Type u)), ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f h (aleph0_le_mk β)

Premises used: Cardinal.infinite_pigeonhole_card_lt, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
hα : ℵ₀ ≤ #α
a : α
ha : #α < #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
⟨a, hα.trans ha.le⟩

Premises used: LT.lt.le, Exists.intro, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
hα : ℵ₀ ≤ #α
a : α
ha : #α < #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
exact ⟨a, hα.trans ha.le⟩
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite α
suffices : Infinite β
⊢ ∃ (a : α), Infinite.{u + 1} (↑(f ⁻¹' {a}) : Type u)

Tactic:
suffices Infinite β from exists_infinite_fiber f h
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite α
⊢ Infinite β

Tactic:
.of_cardinalMk_le h.le

Premises used: LT.lt.le, Infinite.of_cardinalMk_le
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite α
⊢ Infinite β

Tactic:
exact .of_cardinalMk_le h.le
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
simp_rw : ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), Uncountable.{u + 1} (↑(f ⁻¹' {a}) : Type u)

Tactic:
simp_rw [← Cardinal.aleph0_lt_mk_iff, ← aleph_one_le_iff]

Premises used: Cardinal.aleph0_lt_mk_iff, Cardinal.aleph_one_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
inr : ∀ (hα : ℵ₀ ≤ #α), ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
rcases lt_or_ge #α ℵ₀ with hα | hα

Premises used: Cardinal.mk, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : #α < ℵ₀
⊢ (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #β

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : #α < ℵ₀
rw : #α < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
⊢ #α < (ord ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1)).cof

Tactic:
rw [isRegular_aleph_one.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord, Cardinal.isRegular_aleph_one
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : #α < ℵ₀
⊢ #α < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1

Tactic:
hα.trans aleph0_lt_aleph_one

Premises used: Cardinal.aleph0_lt_aleph_one, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : #α < ℵ₀
⊢ #α < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1

Tactic:
exact hα.trans aleph0_lt_aleph_one

Premises used: Cardinal.aleph0_lt_aleph_one, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : #α < ℵ₀
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
exact infinite_pigeonhole_card f ℵ₁ (by simp) aleph0_lt_aleph_one.le
      (by rw [isRegular_aleph_one.cof_ord]; exact hα.trans aleph0_lt_aleph_one)

Premises used: Cardinal.aleph, LT.lt.le, Cardinal.infinite_pigeonhole_card, Cardinal.aleph0_lt_aleph_one, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : ℵ₀ ≤ #α
inr :
  ∀ (a : α) (ha : #α < #(↑(f ⁻¹' {a}) : Type u)),
    ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f h (aleph0_le_mk β)

Premises used: Cardinal.infinite_pigeonhole_card_lt, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : ℵ₀ ≤ #α
a : α
ha : #α < #(↑(f ⁻¹' {a}) : Type u)
inr :
  ∀ (hα : (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ succ #α) (a : α) (ha : #α < #(↑(f ⁻¹' {a}) : Type u)),
    ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)

Tactic:
rw [← Order.succ_le_succ_iff, succ_aleph0] at hα

Premises used: Order.succ_le_succ_iff, Cardinal.succ_aleph0