κ μ : Cardinal
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ 1 < ℵ₀
κ μ : Cardinal
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α ^ ↑Nat.zero < ℵ₀
rw [Nat.cast_zero, power_zero]
no goals
κ μ : Cardinal
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
⊢ 1 < ℵ₀
exact one_lt_aleph0
κ μ : Cardinal
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
n : ℕ
ih : Quotient.mk isEquivalent α ^ ↑n ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α ^ ↑n * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α
κ μ : Cardinal
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
n : ℕ
ih : Quotient.mk isEquivalent α ^ ↑n ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α ^ ↑(Nat.succ n) ≤ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α
rw [Nat.cast_succ, power_add, power_one]
no goals
κ μ : Cardinal
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ Quotient.mk isEquivalent α
n : ℕ
ih : Quotient.mk isEquivalent α ^ ↑n ≤ Quotient.mk isEquivalent α
⊢ Quotient.mk isEquivalent α ^ ↑n * Quotient.mk isEquivalent α ≤ Quotient.mk isEquivalent α * Quotient.mk isEquivalent α
exact mul_le_mul_right' ih _