mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑(⋃ i, ?m.51 ⁻¹' {i}) < #?m.48

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.44

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.43

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ ?m.48 → ?m.50

Tactic:
]

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑(⋃ i, ?m.51 ⁻¹' {i}) < #?m.48

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.44

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.43

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ ?m.48 → ?m.50
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #↑(f ⁻¹' {x})
⊢ ∃ p, #↑p = #↑(f ⁻¹' {x})

Tactic:
]

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

Goal state before:
pp: case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑(Subtype.val ⁻¹' f ⁻¹' {a}) ≤ #↑(f ⁻¹' {a})

Tactic:
]

Goal state after:
case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑(Subtype.val ⁻¹' f ⁻¹' {a}) ≤ #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ IsEmpty { s // Bounded r s }

Tactic:
]

Goal state after:
case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ IsEmpty { s // Bounded r s }
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lift.{v, u} #ι < c

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ c i

Tactic:
]

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ c i
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type (max u_1 u_2)
f : ι → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c

Tactic:
]

Goal state after:
ι : Type (max u_1 u_2)
f : ι → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c

Tactic:
]

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ #↑(⋃ i, 𝒫 {j | r j i}) ≤ #α

Tactic:
]

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ #↑(⋃ i, 𝒫 {j | r j i}) ≤ #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
ho : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
ho : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
ho : o.card < c
⊢ o.card < c

Tactic:
]

Goal state after:
o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
ho : o.card < c
⊢ o.card < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c

Tactic:
]

Goal state after:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : o.card < c
⊢ o.card < c

Tactic:
]

Goal state after:
o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : o.card < c
⊢ o.card < c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ #α ≤ #α

pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ ⨆ i, #↑(𝒫 {j | r j i}) ≤ #α

Tactic:
]

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ ⨆ i, #↑(𝒫 {j | r j i}) ≤ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case e'_3
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = c

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ max c ℵ₀

Tactic:
]

Goal state after:
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
i : α
⊢ 2 ^ #↑{j | r j i} ≤ #α

Tactic:
]

Goal state after:
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
i : α
⊢ 2 ^ #↑{j | r j i} ≤ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀

Tactic:
]

Goal state after:
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ lift.{v, u} #ι < c

Tactic:
]

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c

Tactic:
]

Goal state after:
ι : Type u_1
f : ι → Cardinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ ¬lift.{v, u} #α = lift.{u, v} #β' ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
⊢ #α < ℵ₀

Tactic:
]

Goal state after:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
⊢ #α < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (#α).ord

Tactic:
]

Goal state after:
case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (#α).ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ lift.{v, u} #ι < c

Tactic:
]

Goal state after:
c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ #α ≠ #β ↔ #α ≠ #β

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u}
ι : Type u
f : ι → Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c

Tactic:
]

Goal state after:
c : Cardinal.{u}
ι : Type u
f : ι → Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ lift.{u, v} #β' < lift.{v, u} #α ↔ lift.{u, v} #β' < lift.{v, u} #α

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ #β < #α ↔ #β < #α

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : #α < ℵ₀
⊢ #α < ℵ₀

Tactic:
]

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : #α < ℵ₀
⊢ #α < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)

Tactic:
]

Goal state after:
α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #ι < c

Tactic:
]

Goal state after:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ #α < ℵ_ 1

Tactic:
]

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ #α < ℵ_ 1
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : ℵ_ 1 ≤ succ #α
a : α
ha : #α < #↑(f ⁻¹' {a})
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})

Tactic:
]

Goal state after:
case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : ℵ_ 1 ≤ succ #α
a : α
ha : #α < #↑(f ⁻¹' {a})
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c

Tactic:
]

Goal state after:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ #α < #β ∨ #α ≠ 0 ∧ #β = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #↑s < (type r).cof
⊢ Bounded r s

Tactic:
]

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #↑s < (type r).cof
⊢ Bounded r s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ (type r).cof ≤ #↑s

Tactic:
]

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ (type r).cof ≤ #↑s
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #↑s < c
⊢ (∀ (i : ↑s), #↑(t ↑i ⋯) < c) ↔ ∀ (x : ↑s), #↑(t ↑x ⋯) < c

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
e : α ≃ α × Bool
this : 2 ^ #α ≤ #(Perm (α × Bool))
⊢ 2 ^ #α ≤ #(Perm (α × Bool))

Tactic:
]

Goal state after:
α : Type u
inst✝ : Infinite α
e : α ≃ α × Bool
this : 2 ^ #α ≤ #(Perm (α × Bool))
⊢ 2 ^ #α ≤ #(Perm (α × Bool))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ ∀ (x : α), ∃ y ∈ s, ¬y < x

Tactic:
exact hs

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f ⋯.choose)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f ⋯.choose)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ IsSuccLimit (#α).ord

Tactic:
]

Goal state after:
case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ IsSuccLimit (#α).ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ (f a ^^ false) = (g a ^^ false)

Tactic:
]

Goal state after:
case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ (f a ^^ false) = (g a ^^ false)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ 2 ^ #α = 2 ^ #α

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
a : Ordinal.{u}
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
⊢ #ι < c

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
a : Ordinal.{u}
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
]

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c

Tactic:
]

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
⊢ #β ≤ #↑(range f)

Tactic:
by
  by_contra h
  simp only [not_le] at h
  let u : ∀ b, ∃ a, b ∈ f a := fun b => by simpa using (w.ge :) (Set.mem_univ b)
  let u' : β → range f := fun b => ⟨f (u b).choose, by simp⟩
  have v' : ∀ a, u' ⁻¹' {⟨f a, by simp⟩} ≤ f a := by
    rintro a p m
    have m : f (u p).choose = f a := by simpa [u'] using m
    rw [← m]
    apply fun b => (u b).choose_spec
  obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h
  exact (@Infinite.of_injective _ _ p (inclusion (v' a)) (inclusion_injective _)).false

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α → α) = #(α → α)

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ 2 ^ #α = 2 ^ #α

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord

Tactic:
]

Goal state after:
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case zero
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → nfpFamily f 0 < c.ord

Tactic:
]

Goal state after:
case zero
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → nfpFamily f 0 < c.ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α

Tactic:
]

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ lift.{v, u} #ι < c

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ ℵ₀ = ℵ₀

pp: case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #α ≤ ℵ₀

Tactic:
]

Goal state after:
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #α ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < prod fun x ↦ #α

Tactic:
]

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < prod fun x ↦ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #α = #α

pp: case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ #α

Tactic:
]

Goal state after:
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ max #α ℵ₀ = max #α ℵ₀

Tactic:
]

Goal state after: