case h
α : Type u
β : α → Type u
κ : Cardinal
hκ✝ : (sum fun a => κ ^ (#β a)) ≤ κ
γ : Type u
hκ : (sum fun a => (#γ) ^ (#β a)) ≤ (#γ)
⊢ (#WType β) ≤ (#γ)
α : Type u
β : α → Type u
κ : Cardinal
hκ : (sum fun a => κ ^ (#β a)) ≤ κ
⊢ (#WType β) ≤ κ
induction' κ using Cardinal.inductionOn with γ
case h
α : Type u
β : α → Type u
κ : Cardinal
hκ✝ : (sum fun a => κ ^ (#β a)) ≤ κ
γ : Type u
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ (#WType β) ≤ (#γ)
case h
α : Type u
β : α → Type u
κ : Cardinal
hκ✝ : (sum fun a => κ ^ (#β a)) ≤ κ
γ : Type u
hκ : (sum fun a => (#γ) ^ (#β a)) ≤ (#γ)
⊢ (#WType β) ≤ (#γ)
simp only [Cardinal.power_def, ← Cardinal.mk_sigma, Cardinal.le_def] at hκ
case h.intro
α : Type u
β : α → Type u
κ : Cardinal
hκ✝ : (sum fun a => κ ^ (#β a)) ≤ κ
γ : Type u
hκ : (i : α) × (β i → γ) ↪ γ
⊢ (#WType β) ≤ (#γ)
case h
α : Type u
β : α → Type u
κ : Cardinal
hκ✝ : (sum fun a => κ ^ (#β a)) ≤ κ
γ : Type u
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ (#WType β) ≤ (#γ)
cases' hκ with hκ
no goals
case h.intro
α : Type u
β : α → Type u
κ : Cardinal
hκ✝ : (sum fun a => κ ^ (#β a)) ≤ κ
γ : Type u
hκ : (i : α) × (β i → γ) ↪ γ
⊢ (#WType β) ≤ (#γ)
exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)