α : Type u
inst✝ : Infinite α
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ ((#α) + 1) ^ c
α : Type u
inst✝ : Infinite α
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ (#α) ^ c
refine' le_trans _ (by rw [← add_one_eq (aleph0_le_mk α)])
case h
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (#{ t // (#↑t) ≤ (#β) }) ≤ ((#α) + 1) ^ (#β)
α : Type u
inst✝ : Infinite α
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ ((#α) + 1) ^ c
induction' c using Cardinal.inductionOn with β
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β => β → α) (α ⊕ PUnit) β → { t // (#↑t) ≤ (#β) }

case h.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective ?h.f
case h
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (#{ t // (#↑t) ≤ (#β) }) ≤ ((#α) + 1) ^ (#β)
fapply mk_le_of_surjective
case h.hf.mk.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ∃ a,
    (fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) a =
      { val := s, property := (_ : Nonempty (↑s ↪ β)) }
case h.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }
rintro ⟨s, ⟨g⟩⟩
case h.hf.mk.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
      if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) =
    { val := s, property := (_ : Nonempty (↑s ↪ β)) }
case h.hf.mk.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ∃ a,
    (fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) a =
      { val := s, property := (_ : Nonempty (↑s ↪ β)) }
use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val else Sum.inr ⟨⟩
case h.hf.mk.intro.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) =
    ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case h.hf.mk.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
      if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) =
    { val := s, property := (_ : Nonempty (↑s ↪ β)) }
apply Subtype.eq
case h.hf.mk.intro.a.h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) ↔
    x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case h.hf.mk.intro.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) =
    ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
ext x
case h.hf.mk.intro.a.h.mp
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) →
    x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }

case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) } →
    x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit)
case h.hf.mk.intro.a.h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) ↔
    x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
constructor
no goals
α : Type u
inst✝ : Infinite α
c : Cardinal
⊢ ?m.204381 ≤ (#α) ^ c
rw [← add_one_eq (aleph0_le_mk α)]
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ PUnit) β
⊢ { t // (#↑t) ≤ (#β) }
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β => β → α) (α ⊕ PUnit) β → { t // (#↑t) ≤ (#β) }
intro f
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ PUnit) β
⊢ (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ PUnit) β
⊢ { t // (#↑t) ≤ (#β) }
use Sum.inl ⁻¹' range f
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ PUnit) β
⊢ (#↑(range f)) ≤ (#β)
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ PUnit) β
⊢ (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)
refine' le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) _
no goals
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ PUnit) β
⊢ (#↑(range f)) ≤ (#β)
apply mk_range_le
case h.hf.mk.intro.a.h.mp.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (fun y => if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) y = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case h.hf.mk.intro.a.h.mp
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) →
    x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
rintro ⟨y, h⟩
case h.hf.mk.intro.a.h.mp.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case h.hf.mk.intro.a.h.mp.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (fun y => if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) y = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
dsimp only at h
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) = Sum.inl x
h' : ∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }

case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) = Sum.inl x
h' : ¬∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case h.hf.mk.intro.a.h.mp.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
by_cases h' : ∃ z : s, g z = y
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, ↑g z = y
h : Sum.inl ↑(choose h') = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) = Sum.inl x
h' : ∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
rw [dif_pos h'] at h
case pos.refl
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
y : β
h' : ∃ z, ↑g z = y
h : Sum.inl ↑(choose h') = Sum.inl ↑(choose h')
⊢ ↑(choose h') ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, ↑g z = y
h : Sum.inl ↑(choose h') = Sum.inl x
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
cases Sum.inl.inj h
no goals
case pos.refl
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
y : β
h' : ∃ z, ↑g z = y
h : Sum.inl ↑(choose h') = Sum.inl ↑(choose h')
⊢ ↑(choose h') ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
exact (Classical.choose h').2
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr PUnit.unit = Sum.inl x
h' : ¬∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) = Sum.inl x
h' : ¬∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
rw [dif_neg h'] at h
no goals
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr PUnit.unit = Sum.inl x
h' : ¬∃ z, ↑g z = y
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
cases h
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
⊢ x ∈
    ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit)
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) } →
    x ∈
      ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
          if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit)
intro h
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ x ∈
    ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit)
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
⊢ x ∈
    ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit)
have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ (fun y => if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) (↑g { val := x, property := h }) =
    Sum.inl x
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ x ∈
    ↑((fun f => { val := Sum.inl ⁻¹' range f, property := (_ : (#↑(Sum.inl ⁻¹' range f)) ≤ (#β)) }) fun y =>
        if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit)
use g ⟨x, h⟩
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ (if h_1 : ∃ x_1, ↑g x_1 = ↑g { val := x, property := h } then Sum.inl ↑(choose h_1) else Sum.inr PUnit.unit) =
    Sum.inl x
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ (fun y => if h : ∃ x, ↑g x = y then Sum.inl ↑(choose h) else Sum.inr PUnit.unit) (↑g { val := x, property := h }) =
    Sum.inl x
dsimp only
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ Sum.inl ↑(choose this) = Sum.inl x
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ (if h_1 : ∃ x_1, ↑g x_1 = ↑g { val := x, property := h } then Sum.inl ↑(choose h_1) else Sum.inr PUnit.unit) =
    Sum.inl x
rw [dif_pos this]
case h.hf.mk.intro.a.h.mpr.e_val
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ ↑(choose this) = x
case h.hf.mk.intro.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ Sum.inl ↑(choose this) = Sum.inl x
congr
case h.hf.mk.intro.a.h.mpr.e_val
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this✝ : ∃ z, ↑g z = ↑g { val := x, property := h }
this : choose this✝ = { val := x, property := h }
⊢ ↑(choose this✝) = x

case this
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ choose this = { val := x, property := h }
case h.hf.mk.intro.a.h.mpr.e_val
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ ↑(choose this) = x
suffices : Classical.choose this = ⟨x, h⟩
case this
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ choose this = { val := x, property := h }
case h.hf.mk.intro.a.h.mpr.e_val
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this✝ : ∃ z, ↑g z = ↑g { val := x, property := h }
this : choose this✝ = { val := x, property := h }
⊢ ↑(choose this✝) = x

case this
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ choose this = { val := x, property := h }
exact congr_arg Subtype.val this
case this.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ Embedding.toFun g (choose this) = Embedding.toFun g { val := x, property := h }
case this
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ choose this = { val := x, property := h }
apply g.2
no goals
case this.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑{ val := s, property := (_ : Nonempty (↑s ↪ β)) }
this : ∃ z, ↑g z = ↑g { val := x, property := h }
⊢ Embedding.toFun g (choose this) = Embedding.toFun g { val := x, property := h }
exact Classical.choose_spec this