-- 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 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 })

Tactic:
have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩

Result:
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 })

Proof state:
case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #↑(Sum.inl ⁻¹' range f) ≤ #β

Tactic:
refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_

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

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

Tactic:
apply mk_range_le

Result:
no goals

Proof state:
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, ⋯⟩

Tactic:
apply Subtype.eq

Result:
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, ⋯⟩

Proof state:
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, h⟩

Tactic:
apply g.2

Result:
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⟩

Proof state:
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

Tactic:
suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this

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, h⟩

Proof state:
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, ⋯⟩

Tactic:
by_cases h' : ∃ z : s, g z = y

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

Proof state:
case neg
α : 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
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
rw [dif_neg h'] at h

Result:
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, ⋯⟩

Proof state:
case pos
α : 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
h' : ∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
rw [dif_pos h'] at h

Result:
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, ⋯⟩

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⟩
⊢ (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

Tactic:
dsimp only

Result:
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

Proof state:
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ ?m.84063 ≤ #α ^ c

Tactic:
rw [← add_one_eq (aleph0_le_mk α)]

Result:
no goals

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

Tactic:
use Sum.inl ⁻¹' range f

Result:
case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β => β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #↑(Sum.inl ⁻¹' range f) ≤ #β