α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (x : (Quotient.out (ord (aleph 1))).α),
    (∀ (y : (Quotient.out (ord (aleph 1))).α),
        WellOrder.r (Quotient.out (ord (aleph 1))) y x → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀) →
      (#↑(generateMeasurableRec s x)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
apply (aleph 1).ord.out.wo.wf.induction i
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (x : (Quotient.out (ord (aleph 1))).α),
    (∀ (y : (Quotient.out (ord (aleph 1))).α),
        WellOrder.r (Quotient.out (ord (aleph 1))) y x → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀) →
      (#↑(generateMeasurableRec s x)) ≤ max (#↑s) 2 ^ ℵ₀
intro i IH
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
have A := aleph0_le_aleph 1
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
have B : aleph 1 ≤ max (#s) 2 ^ aleph0.{u} :=
  aleph_one_le_continuum.trans (power_le_power_right (le_max_right _ _))
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
have C : ℵ₀ ≤ max (#s) 2 ^ aleph0.{u} := A.trans B
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
have J : (#⋃ j : Iio i, generateMeasurableRec s j.1) ≤ max (#s) 2 ^ aleph0.{u} := by
  refine (mk_iUnion_le _).trans ?_
  have D : (⨆ j : Iio i, #generateMeasurableRec s j) ≤ _ := ciSup_le' fun ⟨j, hj⟩ => IH j hj
  apply (mul_le_mul' ((mk_subtype_le _).trans (aleph 1).mk_ord_out.le) D).trans
  rw [mul_eq_max A C]
  exact max_le B le_rfl
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑((s ∪ {∅} ∪ compl '' ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ∪ range fun f => ⋃ (n : ℕ), ↑(f n))) ≤
    max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
rw [generateMeasurableRec]
case h1.h1.h1
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑s) ≤ max (#↑s) 2 ^ ℵ₀

case h1.h1.h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑{∅}) ≤ max (#↑s) 2 ^ ℵ₀

case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(range fun f => ⋃ (n : ℕ), ↑(f n))) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑((s ∪ {∅} ∪ compl '' ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ∪ range fun f => ⋃ (n : ℕ), ↑(f n))) ≤
    max (#↑s) 2 ^ ℵ₀
apply_rules [(mk_union_le _ _).trans, add_le_of_le C, mk_image_le.trans]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ ((#↑(Iio i)) * ⨆ (i_1 : ↑(Iio i)), #↑(generateMeasurableRec s ↑i_1)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
refine (mk_iUnion_le _).trans ?_
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : (⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ ((#↑(Iio i)) * ⨆ (i_1 : ↑(Iio i)), #↑(generateMeasurableRec s ↑i_1)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ ((#↑(Iio i)) * ⨆ (i_1 : ↑(Iio i)), #↑(generateMeasurableRec s ↑i_1)) ≤ max (#↑s) 2 ^ ℵ₀
have D : (⨆ j : Iio i, #generateMeasurableRec s j) ≤ _ := ciSup_le' fun ⟨j, hj⟩ => IH j hj
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : (⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ aleph 1 * max (#↑s) 2 ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : (⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ ((#↑(Iio i)) * ⨆ (i_1 : ↑(Iio i)), #↑(generateMeasurableRec s ↑i_1)) ≤ max (#↑s) 2 ^ ℵ₀
apply (mul_le_mul' ((mk_subtype_le _).trans (aleph 1).mk_ord_out.le) D).trans
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : (⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ max (aleph 1) (max (#↑s) 2 ^ ℵ₀) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : (⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ aleph 1 * max (#↑s) 2 ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
rw [mul_eq_max A C]
no goals
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : (⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ max (aleph 1) (max (#↑s) 2 ^ ℵ₀) ≤ max (#↑s) 2 ^ ℵ₀
exact max_le B le_rfl
no goals
case h1.h1.h1
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑s) ≤ max (#↑s) 2 ^ ℵ₀
exact (le_max_left _ _).trans (self_le_power _ one_lt_aleph0.le)
case h1.h1.h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ 1 ≤ max (#↑s) 2 ^ ℵ₀
case h1.h1.h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑{∅}) ≤ max (#↑s) 2 ^ ℵ₀
rw [mk_singleton]
no goals
case h1.h1.h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ 1 ≤ max (#↑s) 2 ^ ℵ₀
exact one_lt_aleph0.le.trans C
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#ℕ → ↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(range fun f => ⋃ (n : ℕ), ↑(f n))) ≤ max (#↑s) 2 ^ ℵ₀
apply mk_range_le.trans
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#ℕ → ↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
simp only [mk_pi, prod_const, lift_uzero, mk_denumerable, lift_aleph0]
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
this : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ^ ℵ₀ ≤ (max (#↑s) 2 ^ ℵ₀) ^ ℵ₀
⊢ (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
⊢ (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
have := @power_le_power_right _ _ ℵ₀ J
no goals
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → (#↑(generateMeasurableRec s y)) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
this : (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ^ ℵ₀ ≤ (max (#↑s) 2 ^ ℵ₀) ^ ℵ₀
⊢ (#↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
rwa [← power_mul, aleph0_mul_aleph0] at this