-- Mathlib/Data/W/Cardinal.lean
theorem cardinalMk_le_max_aleph0_of_finite' [∀ a, Finite (β a)] :
    #(WType β) ≤ max (lift.{v} #α) ℵ₀ :=
  (isEmpty_or_nonempty α).elim
    (by
      intro h
      rw [Cardinal.mk_eq_zero (WType β)]
      exact zero_le _)
    fun hn =>
    let m := max (lift.{v} #α) ℵ₀
    cardinalMk_le_of_le' <|
      calc
        (Cardinal.sum fun a => m ^ lift.{u} #(β a)) ≤ lift.{v} #α * ⨆ a, m ^ lift.{u} #(β a) :=
          Cardinal.sum_le_iSup_lift _
        _ ≤ m * ⨆ a, m ^ lift.{u} #(β a) := mul_le_mul' (le_max_left _ _) le_rfl
        _ = m :=
          mul_eq_left (le_max_right _ _)
              (ciSup_le' fun _ => pow_le (le_max_right _ _) (lt_aleph0_of_finite _)) <|
            pos_iff_ne_zero.1 <|
              Order.succ_le_iff.1
                (by
                  rw [succ_zero]
                  obtain ⟨a⟩ : Nonempty α := hn
                  refine le_trans ?_ (le_ciSup (bddAbove_range _) a)
                  rw [← power_zero]
                  exact
                    power_le_power_left
                      (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _))

Proof state:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ #(WType β) ≤ lift.{v, u} #α ⊔ ℵ₀

Tactic:
rw [Cardinal.mk_eq_zero (WType β)]

Result:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ 0 ≤ lift.{v, u} #α ⊔ ℵ₀

Proof state:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
⊢ 1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)

Tactic:
obtain ⟨a⟩ : Nonempty α := hn

Result:
case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ 1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)

Proof state:
case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ ?intro ^ 0 ≤ m ^ lift.{u, v} #(β a)

case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ Cardinal.{max u v}

Tactic:
exact
  power_le_power_left
    (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ 0 ≤ lift.{v, u} #α ⊔ ℵ₀

Tactic:
exact zero_le _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
⊢ IsEmpty α → #(WType β) ≤ lift.{v, u} #α ⊔ ℵ₀

Tactic:
intro h

Result:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ #(WType β) ≤ lift.{v, u} #α ⊔ ℵ₀

Proof state:
case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ 1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)

Tactic:
refine le_trans ?_ (le_ciSup (bddAbove_range _) a)

Result:
case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ 1 ≤ m ^ lift.{u, v} #(β a)

Proof state:
case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ 1 ≤ m ^ lift.{u, v} #(β a)

Tactic:
rw [← power_zero]

Result:
case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ ?intro ^ 0 ≤ m ^ lift.{u, v} #(β a)

case intro
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
a : α
⊢ Cardinal.{max u v}

Proof state:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
⊢ Order.succ 0 ≤ ⨆ a, m ^ lift.{u, v} #(β a)

Tactic:
rw [succ_zero]

Result:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{max u v} := lift.{v, u} #α ⊔ ℵ₀
⊢ 1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)