-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : Ordinal.{v}) :
    #(generateMeasurableRec s i) ≤ max #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
⊢ 2 ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2)

Tactic:
rw [lift_max, Cardinal.lift_ofNat]

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:
α : 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) ^ ℵ₀

Tactic:
intro i IH hi

Result:
α : 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) ^ ℵ₀

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) ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
have B := aleph0_le_continuum.trans A

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) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ #↑(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 : 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) ^ ℵ₀

Tactic:
have H := card_le_of_le_ord 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) ^ ℵ₀
H : (Ordinal.lift.{u, v} i).card ≤ ℵ_ 1
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2) ^ ℵ₀

Proof state:
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) ^ ℵ₀

Tactic:
rw [mk_singleton]

Result:
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) ^ ℵ₀
⊢ 1 ≤ (#↑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 : (Ordinal.lift.{u, v} i).card ≤ ℵ_ 1
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2) ^ ℵ₀

Tactic:
rw [← Ordinal.lift_card] at H

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
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (#↑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) ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} ((#↑s ⊔ 2) ^ ℵ₀)

Tactic:
rw [lift_power, lift_aleph0]

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) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (#↑s ⊔ 2) ^ ℵ₀

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

Tactic:
exact this _ le_rfl

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) ^ ℵ₀
⊢ ∀ j < i, #↑(generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
intro j hj

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) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
j : Ordinal.{v}
hj : 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) ^ ℵ₀
j : Ordinal.{v}
hj : j < i
⊢ #↑(generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
exact IH j hj (hj.trans_le hi).le

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) ^ ℵ₀
⊢ #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
apply mk_iUnion_Ordinal_lift_le_of_le _ B _

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) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ ∀ j < i, #↑(generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀

α : 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) ^ ℵ₀)

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) ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
rw [generateMeasurableRec]

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) ^ ℵ₀
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) ^ ℵ₀

Proof state:
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) ^ ℵ₀

Tactic:
exact (self_le_power _ one_le_aleph0).trans (power_le_power_right (le_max_left _ _))

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 : 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

Tactic:
exact le_max_right _ _

Result:
no goals