[GOAL]
α : Type u
β : α → Type u
⊢ #(WType β) = sum fun a => #(WType β) ^ #(β a)
[PROOFSTEP]
simp only [Cardinal.power_def, ← Cardinal.mk_sigma]
[GOAL]
α : Type u
β : α → Type u
⊢ #(WType β) = #((i : α) × (β i → WType β))
[PROOFSTEP]
exact mk_congr (equivSigma β)
[GOAL]
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a => κ ^ #(β a)) ≤ κ
⊢ #(WType β) ≤ κ
[PROOFSTEP]
induction' κ using Cardinal.inductionOn with γ
[GOAL]
case h
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ✝ : (sum fun a => κ ^ #(β a)) ≤ κ
γ : Type u
hκ : (sum fun a => #γ ^ #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
[PROOFSTEP]
simp only [Cardinal.power_def, ← Cardinal.mk_sigma, Cardinal.le_def] at hκ 
[GOAL]
case h
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ✝ : (sum fun a => κ ^ #(β a)) ≤ κ
γ : Type u
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ #(WType β) ≤ #γ
[PROOFSTEP]
cases' hκ with hκ
[GOAL]
case h.intro
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ✝ : (sum fun a => κ ^ #(β a)) ≤ κ
γ : Type u
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ
[PROOFSTEP]
exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ IsEmpty α → #(WType β) ≤ max #α ℵ₀
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ #(WType β) ≤ max #α ℵ₀
[PROOFSTEP]
rw [Cardinal.mk_eq_zero (WType β)]
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ 0 ≤ max #α ℵ₀
[PROOFSTEP]
exact zero_le _
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{u} := max #α ℵ₀
⊢ Order.succ 0 ≤ ⨆ (a : α), m ^ #(β a)
[PROOFSTEP]
rw [succ_zero]
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{u} := max #α ℵ₀
⊢ 1 ≤ ⨆ (a : α), m ^ #(β a)
[PROOFSTEP]
obtain ⟨a⟩ : Nonempty α := hn
[GOAL]
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{u} := max #α ℵ₀
a : α
⊢ 1 ≤ ⨆ (a : α), m ^ #(β a)
[PROOFSTEP]
refine' le_trans _ (le_ciSup (bddAbove_range.{u, u} _) a)
[GOAL]
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{u} := max #α ℵ₀
a : α
⊢ 1 ≤ m ^ #(β a)
[PROOFSTEP]
rw [← power_zero]
[GOAL]
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{u} := max #α ℵ₀
a : α
⊢ ?m.2506 ^ 0 ≤ m ^ #(β a)
α : Type u β : α → Type u inst✝ : ∀ (a : α), Finite (β a) m : Cardinal.{u} := max #α ℵ₀ a : α ⊢ Cardinal.{u}
[PROOFSTEP]
exact power_le_power_left (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _)
