-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
/-- Bounds the cardinal of an ordinal-indexed union of sets. -/
lemma mk_iUnion_Ordinal_lift_le_of_le {β : Type v} {o : Ordinal.{u}} {c : Cardinal.{v}}
    (ho : lift.{v} o.card ≤ lift.{u} c) (hc : ℵ₀ ≤ c) (A : Ordinal → Set β)
    (hA : ∀ j < o, #(A j) ≤ c) : #(⋃ j < o, A j) ≤ c

Proof state:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(sSup (range ((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm))) ≤ c

Tactic:
rw [← lift_le.{u}]

Result:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u, v} #↑(sSup (range ((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm))) ≤ lift.{u, v} c

Proof state:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{v, u} o.card * ⨆ i, lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤ lift.{u, v} c * lift.{u, v} c

Tactic:
refine mul_le_mul' ho (ciSup_le' ?_)

Result:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ ∀ (i : o.toType), lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤ lift.{u, v} c

Proof state:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Tactic:
simp_rw [← mem_Iio, biUnion_eq_iUnion, iUnion, iSup, ← o.enumIsoToType.symm.surjective.range_comp]

Result:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(sSup (range ((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm))) ≤ c

Proof state:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{v, u} #o.toType * ⨆ i, lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤
    lift.{u, v} c * lift.{u, v} c

Tactic:
rw [mk_toType]

Result:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{v, u} o.card * ⨆ i, lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤ lift.{u, v} c * lift.{u, v} c

Proof state:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ ∀ (i : o.toType), lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤ lift.{u, v} c

Tactic:
intro i

Result:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
i : o.toType
⊢ lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤ lift.{u, v} c

Proof state:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
i : o.toType
⊢ lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤ lift.{u, v} c

Tactic:
simpa using hA _ (o.enumIsoToType.symm i).2

Result:
no goals

Proof state:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u, v} #↑(sSup (range ((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm))) ≤ lift.{u, v} c

Tactic:
apply ((mk_iUnion_le_lift _).trans _).trans_eq (mul_eq_self (aleph0_le_lift.2 hc))

Result:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{v, u} #o.toType * ⨆ i, lift.{u, v} #↑(((fun x => A ↑x) ∘ ⇑o.enumIsoToType.symm) i) ≤
    lift.{u, v} c * lift.{u, v} c