case a
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c

case a
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ = c
apply le_antisymm
case h.e'_3
c : Cardinal
h : ℵ₀ ≤ c
⊢ c = c ^ 1
case a
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀
convert le_powerlt c one_lt_aleph0
no goals
case h.e'_3
c : Cardinal
h : ℵ₀ ≤ c
⊢ c = c ^ 1
rw [power_one]
case a
c : Cardinal
h : ℵ₀ ≤ c
⊢ ∀ (x : Cardinal), x < ℵ₀ → c ^ x ≤ c
case a
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c
rw [powerlt_le]
case a
c : Cardinal
h : ℵ₀ ≤ c
c' : Cardinal
⊢ c' < ℵ₀ → c ^ c' ≤ c
case a
c : Cardinal
h : ℵ₀ ≤ c
⊢ ∀ (x : Cardinal), x < ℵ₀ → c ^ x ≤ c
intro c'
case a
c : Cardinal
h : ℵ₀ ≤ c
c' : Cardinal
⊢ (∃ n, c' = ↑n) → c ^ c' ≤ c
case a
c : Cardinal
h : ℵ₀ ≤ c
c' : Cardinal
⊢ c' < ℵ₀ → c ^ c' ≤ c
rw [lt_aleph0]
case a.intro
c : Cardinal
h : ℵ₀ ≤ c
n : ℕ
⊢ c ^ ↑n ≤ c
case a
c : Cardinal
h : ℵ₀ ≤ c
c' : Cardinal
⊢ (∃ n, c' = ↑n) → c ^ c' ≤ c
rintro ⟨n, rfl⟩
no goals
case a.intro
c : Cardinal
h : ℵ₀ ≤ c
n : ℕ
⊢ c ^ ↑n ≤ c
apply power_nat_le h