-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : Ordinal.{v}) :
    #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀

Proof state:
case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ^ ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
have := @power_le_power_right _ _ ℵ₀ C

Result:
case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
this : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ^ ℵ₀ ≤ ((#↑s ⊔ 2) ^ ℵ₀) ^ ℵ₀
⊢ #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ^ ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀

Proof state:
case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #(ℕ → ↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j)) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
simp only [mk_pi, prod_const, Cardinal.lift_uzero, mk_denumerable, lift_aleph0]

Result:
case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ^ ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀

Proof state:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑((s ∪ {∅} ∪ compl '' ⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ∪ range fun f => ⋃ n, ↑(f n)) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
apply_rules [(mk_union_le _ _).trans, add_le_of_le (aleph_one_le_continuum.trans A),
  mk_image_le.trans]

Result:
case h1.h1.h1
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑s ≤ (#↑s ⊔ 2) ^ ℵ₀

case h1.h1.h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑{∅} ≤ (#↑s ⊔ 2) ^ ℵ₀

case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑(range fun f => ⋃ n, ↑(f n)) ≤ (#↑s ⊔ 2) ^ ℵ₀

Proof state:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ (ℵ_ 1).ord
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
H : Cardinal.lift.{u, v} i.card ≤ ℵ_ 1
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2) ^ ℵ₀

Tactic:
apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _

Result:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ (ℵ_ 1).ord
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
H : Cardinal.lift.{u, v} i.card ≤ ℵ_ 1
⊢ 2 ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2)

Proof state:
case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑(range fun f => ⋃ n, ↑(f n)) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
apply mk_range_le.trans

Result:
case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #(ℕ → ↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j)) ≤ (#↑s ⊔ 2) ^ ℵ₀

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
obtain hi | hi := le_or_lt i ω₁

Result:
case inl
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

case inr
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : ω_ 1 < i
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Proof state:
case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
this : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ^ ℵ₀ ≤ ((#↑s ⊔ 2) ^ ℵ₀) ^ ℵ₀
⊢ #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ^ ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
rwa [← power_mul, aleph0_mul_aleph0] at this

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2) ^ ℵ₀

Tactic:
rw [← Ordinal.lift_le.{u}, lift_omega, Ordinal.lift_one, ← ord_aleph] at hi

Result:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ (ℵ_ 1).ord
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2) ^ ℵ₀

Proof state:
case inl
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
exact this i hi

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
i✝ i : Ordinal.{v}
⊢ i ≤ ω_ 1 → #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
apply WellFoundedLT.induction i

Result:
α : Type u
s : Set (Set α)
i✝ i : Ordinal.{v}
⊢ ∀ (x : Ordinal.{v}),
    (∀ y < x, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀) →
      x ≤ ω_ 1 → #↑(generateMeasurableRec s x) ≤ (#↑s ⊔ 2) ^ ℵ₀

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
⊢ ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
intro i

Result:
α : Type u
s : Set (Set α)
i✝ i : Ordinal.{v}
⊢ i ≤ ω_ 1 → #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Proof state:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
have A : 𝔠 ≤ max #s 2 ^ ℵ₀ := power_le_power_right (le_max_right _ _)

Result:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀