-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_bounded_set_le_of_infinite (α : Type u) [Infinite α] (c : Cardinal) :
    #{ t : Set α // #t ≤ c } ≤ #α ^ c

Proof state:
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
cases Sum.inl.inj h

Result:
case pos.refl
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl ↑(Classical.choose h')
⊢ ↑(Classical.choose h') ∈ ↑⟨s, ⋯⟩

Proof state:
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β => β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t // #↑t ≤ #β }

Tactic:
intro f

Result:
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ { t // #↑t ≤ #β }

Proof state:
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr { down := 0 } = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
cases h

Result:
no goals

Proof state:
case h.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
        if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) =
    ↑⟨s, ⋯⟩

Tactic:
ext x

Result:
case h.a.h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) ↔
    x ∈ ↑⟨s, ⋯⟩

Proof state:
case h.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })

Tactic:
intro h

Result:
case h.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
⊢ x ∈
    ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
        if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })

Proof state:
case h.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ x ∈
    ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
        if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })

Tactic:
use g ⟨x, h⟩

Result:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ (fun y => if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) (g ⟨x, h⟩) = Sum.inl x

Proof state:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ (if h_1 : ∃ x_1, g x_1 = g ⟨x, h⟩ then Sum.inl ↑(Classical.choose h_1) else Sum.inr { down := 0 }) = Sum.inl x

Tactic:
rw [dif_pos this]

Result:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ Sum.inl ↑(Classical.choose this) = Sum.inl x

Proof state:
case h.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 ↑(Classical.choose h) else Sum.inr { down := 0 }) y = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
dsimp only at h

Result:
case h.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 ↑(Classical.choose h) else Sum.inr { down := 0 }) = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩

Proof state:
case h.a.h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) ↔
    x ∈ ↑⟨s, ⋯⟩

Tactic:
constructor

Result:
case h.a.h.mp
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) →
    x ∈ ↑⟨s, ⋯⟩

case h.a.h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })

Proof state:
case pos.refl
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl ↑(Classical.choose h')
⊢ ↑(Classical.choose h') ∈ ↑⟨s, ⋯⟩

Tactic:
exact (Classical.choose h').2

Result:
no goals

Proof state:
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #α ^ c

Tactic:
refine le_trans ?_ (by rw [← add_one_eq (aleph0_le_mk α)])

Result:
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α + 1) ^ c

Proof state:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ Sum.inl ↑(Classical.choose this) = Sum.inl x

Tactic:
congr

Result:
case h.e_val
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ ↑(Classical.choose this) = x

Proof state:
case h.hf.mk.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ∃ a, (fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) a = ⟨s, ⋯⟩

Tactic:
use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
             else Sum.inr (ULift.up 0)

Result:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
      if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) =
    ⟨s, ⋯⟩

Proof state:
case h.a.h.mp
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈
      ↑((fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y =>
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) →
    x ∈ ↑⟨s, ⋯⟩

Tactic:
rintro ⟨y, h⟩

Result:
case h.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 ↑(Classical.choose h) else Sum.inr { down := 0 }) y = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩

Proof state:
case h
α : Type u
inst✝ : Infinite α
β : Type u
⊢ #{ t // #↑t ≤ #β } ≤ (#α + 1) ^ #β

Tactic:
fapply mk_le_of_surjective

Result:
case h.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β => β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t // #↑t ≤ #β }

case h.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective ?h.f

Proof state:
case h.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩

Tactic:
rintro ⟨s, ⟨g⟩⟩

Result:
case h.hf.mk.intro
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ∃ a, (fun f => ⟨Sum.inl ⁻¹' range f, ⋯⟩) a = ⟨s, ⋯⟩

Proof state:
case h.e_val.a
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ g.toFun (Classical.choose this) = g.toFun ⟨x, h⟩

Tactic:
exact Classical.choose_spec this

Result:
no goals

Proof state:
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α + 1) ^ c

Tactic:
induction' c using Cardinal.inductionOn with β

Result:
case h
α : Type u
inst✝ : Infinite α
β : Type u
⊢ #{ t // #↑t ≤ #β } ≤ (#α + 1) ^ #β