awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ ∀ (x : Ordinal.{u_1}),
    (∀ y < x, generateMeasurableRec s y ⊆ {t : Set α | GenerateMeasurable s t}) →
      generateMeasurableRec s x ⊆ {t : Set α | GenerateMeasurable s t}

Tactic:
exact fun i IH t ht => generateMeasurableRec_induction .basic .empty
    (fun u _ ⟨j, hj, hj'⟩ => .compl _ (IH j hj hj')) (fun f H => .iUnion _ fun n => (H n).1) ht
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
apply :
  {t : Set α | GenerateMeasurable s t} ⊆ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
⊢ {t : Set α | GenerateMeasurable s t} = generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
apply (generateMeasurableRec_subset s _).antisymm'

Premises used: MeasurableSpace.generateMeasurableRec_subset, HasSubset.Subset.antisymm'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t u : Set α
hu : u ∈ s
⊢ u ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
self_subset_generateMeasurableRec s _ hu

Premises used: MeasurableSpace.self_subset_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t u : Set α
hu : u ∈ s
⊢ u ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
exact self_subset_generateMeasurableRec s _ hu

Premises used: MeasurableSpace.self_subset_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
⊢ ∅ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
empty_mem_generateMeasurableRec s _

Premises used: MeasurableSpace.empty_mem_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
⊢ ∅ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
exact empty_mem_generateMeasurableRec s _

Premises used: MeasurableSpace.empty_mem_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t u : Set α
h : GenerateMeasurable s u
IH : u ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
⊢ ∃ (i : Ordinal.{u_1}) (_ : i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1), u ∈ generateMeasurableRec s i

Tactic:
rw [generateMeasurableRec_omega_one, mem_iUnion₂] at IH

Premises used: Set.mem_iUnion₂, MeasurableSpace.generateMeasurableRec_omega_one
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t u : Set α
h : GenerateMeasurable s u
IH : ∃ (i : Ordinal.{u_1}) (_ : i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1), u ∈ generateMeasurableRec s i
compl :
  ∀ (i : Ordinal.{u_1}) (hi : i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1) (hi' : u ∈ generateMeasurableRec s i),
    uᶜ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
⊢ uᶜ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
obtain ⟨i, hi, hi'⟩ := IH
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t u : Set α
h : GenerateMeasurable s u
i : Ordinal.{u_1}
hi : i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
hi' : u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
generateMeasurableRec_mono _ ((isSuccLimit_omega 1).succ_lt hi).le
      (compl_mem_generateMeasurableRec (Order.lt_succ i) hi')

Premises used: LT.lt.le, Order.lt_succ, Order.IsSuccLimit.succ_lt, MeasurableSpace.generateMeasurableRec_mono, MeasurableSpace.compl_mem_generateMeasurableRec, OfNat.ofNat, Cardinal.isSuccLimit_omega
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t u : Set α
h : GenerateMeasurable s u
i : Ordinal.{u_1}
hi : i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
hi' : u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
exact generateMeasurableRec_mono _ ((isSuccLimit_omega 1).succ_lt hi).le
      (compl_mem_generateMeasurableRec (Order.lt_succ i) hi')

Premises used: LT.lt.le, Order.lt_succ, Order.IsSuccLimit.succ_lt, MeasurableSpace.generateMeasurableRec_mono, MeasurableSpace.compl_mem_generateMeasurableRec, OfNat.ofNat, Cardinal.isSuccLimit_omega
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
f : ℕ → Set α
h : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
⊢ ∀ (n : ℕ), ∃ i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1, f n ∈ generateMeasurableRec s i

Tactic:
simp_rw [generateMeasurableRec_omega_one, mem_iUnion₂, exists_prop] at IH

Premises used: exists_prop, Set.mem_iUnion₂, MeasurableSpace.generateMeasurableRec_omega_one
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
f : ℕ → Set α
h : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), ∃ i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1, f n ∈ generateMeasurableRec s i
⊢ ⋃ (i : ℕ), f i ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
iUnion_mem_generateMeasurableRec IH

Premises used: MeasurableSpace.iUnion_mem_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
f : ℕ → Set α
h : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), ∃ i < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1, f n ∈ generateMeasurableRec s i
⊢ ⋃ (i : ℕ), f i ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
exact iUnion_mem_generateMeasurableRec IH

Premises used: MeasurableSpace.iUnion_mem_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : Membership.mem (γ := Set (Set α)) {t : Set α | GenerateMeasurable s t} t
basic : ∀ (u : Set α) (hu : u ∈ s), u ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
empty : ∅ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
compl :
  ∀ (u : Set α),
    GenerateMeasurable s u →
      ∀ (IH : u ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)),
        uᶜ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (n : ℕ), GenerateMeasurable s (f n)) →
      ∀ (IH : ∀ (n : ℕ), f n ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)),
        ⋃ (i : ℕ), f i ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
⊢ t ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)

Tactic:
induction ht with
  | basic u hu => exact self_subset_generateMeasurableRec s _ hu
  | empty => exact empty_mem_generateMeasurableRec s _
  | compl u _ IH =>
    rw [generateMeasurableRec_omega_one, mem_iUnion₂] at IH
    obtain ⟨i, hi, hi'⟩ := IH
    exact generateMeasurableRec_mono _ ((isSuccLimit_omega 1).succ_lt hi).le
      (compl_mem_generateMeasurableRec (Order.lt_succ i) hi')
  | iUnion f _ IH =>
    simp_rw [generateMeasurableRec_omega_one, mem_iUnion₂, exists_prop] at IH
    exact iUnion_mem_generateMeasurableRec IH

Premises used: Compl.compl, exists_prop, Set.mem_iUnion₂, MeasurableSpace.empty_mem_generateMeasurableRec, MeasurableSpace.generateMeasurableRec_omega_one, Set.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ≤ i
apply : generateMeasurableRec s i ≤ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
⊢ generateMeasurableRec s i = generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)

Tactic:
apply (generateMeasurableRec_mono s hi).antisymm'

Premises used: LE.le.antisymm', MeasurableSpace.generateMeasurableRec_mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ≤ i
rw : generateMeasurableRec s i ≤ {t : Set α | GenerateMeasurable s t}
⊢ generateMeasurableRec s i ≤ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)

Tactic:
rw [← generateMeasurable_eq_rec]

Premises used: MeasurableSpace.generateMeasurable_eq_rec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ≤ i
⊢ generateMeasurableRec s i ≤ {t : Set α | GenerateMeasurable s t}

Tactic:
generateMeasurableRec_subset s i

Premises used: MeasurableSpace.generateMeasurableRec_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ≤ i
⊢ generateMeasurableRec s i ≤ {t : Set α | GenerateMeasurable s t}

Tactic:
exact generateMeasurableRec_subset s i

Premises used: MeasurableSpace.generateMeasurableRec_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this :
  ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
inl :
  ∀ (hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1),
    #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
inr :
  ∀ (hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 < i),
    #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

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

Premises used: Ordinal.omega, le_or_gt, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this :
  ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
this i hi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this :
  ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
exact this i hi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this :
  ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 < i
inr :
  #(↑(generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
rw [generateMeasurableRec_of_omega_one_le s hi.le]

Premises used: MeasurableSpace.generateMeasurableRec_of_omega_one_le, LT.lt.le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this :
  ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 < i
⊢ #(↑(generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
this _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this :
  ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 < i
⊢ #(↑(generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
exact this _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
suffices :
  ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
suffices ∀ i ≤ ω₁, #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀ by
    obtain hi | hi := le_or_gt i ω₁
    · exact this i hi
    · rw [generateMeasurableRec_of_omega_one_le s hi.le]
      exact this _ le_rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i : Ordinal.{v}
apply :
  ∀ (x : Ordinal.{v}),
    (∀ y < x,
        y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
          #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀) →
      x ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
        #(↑(generateMeasurableRec s x) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 → #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
apply WellFoundedLT.induction i

Premises used: WellFoundedLT.induction
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
⊢ 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
have A : 𝔠 ≤ max #s 2 ^ ℵ₀ := power_le_power_right (le_max_right _ _)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
have B := aleph0_le_continuum.trans A
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
apply : ∀ j < i, #(↑(generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
apply₁ : Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2 ^ ℵ₀)
⊢ #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
apply mk_biUnion_le_of_le_lift _ B _

Premises used: Cardinal.mk_biUnion_le_of_le_lift
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
j : Ordinal.{v}
hj : j < i
⊢ #(↑(generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

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

Premises used: LT.lt.le, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
j : Ordinal.{v}
hj : j < i
⊢ #(↑(generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

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

Premises used: LT.lt.le, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
rw : Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2) ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2 ^ ℵ₀)

Tactic:
rw [lift_power, lift_aleph0]

Premises used: Cardinal.lift_aleph0, Cardinal.lift_power
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)

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

Premises used: Ordinal.lift_one, Cardinal.ord_aleph, Ordinal.lift_omega
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi₁ : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
⊢ 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

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

Premises used: Ordinal.lift_one, Cardinal.ord_aleph, Ordinal.lift_omega
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi₁ : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
A₁ : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

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

Premises used: Ordinal.lift_one, Cardinal.ord_aleph, Ordinal.lift_omega
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ (Ordinal.lift.{u, v} i).card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1

Tactic:
have H := card_le_of_le_ord hi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
H : (Ordinal.lift.{u, v} i).card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1
⊢ Cardinal.lift.{u, v} i.card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1

Tactic:
rw [← Ordinal.lift_card] at H

Premises used: Ordinal.lift_card
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
H : Cardinal.lift.{u, v} i.card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1
apply : 2 ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2)
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2) ^ ℵ₀

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

Premises used: Cardinal.power_le_power_right, Cardinal.aleph_one_le_continuum, LE.le.trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
H : Cardinal.lift.{u, v} i.card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1
rw : 2 ≤ max (Cardinal.lift.{v, u} #(↑s : Type u)) 2
⊢ 2 ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2)

Tactic:
rw [lift_max, Cardinal.lift_ofNat]

Premises used: Cardinal.lift_ofNat, Cardinal.lift_max
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
H : Cardinal.lift.{u, v} i.card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1
⊢ 2 ≤ max (Cardinal.lift.{v, u} #(↑s : Type u)) 2

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ ord ((ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1)
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
H : Cardinal.lift.{u, v} i.card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1
⊢ 2 ≤ max (Cardinal.lift.{v, u} #(↑s : Type u)) 2

Tactic:
exact le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
have C : #(⋃ j < i, generateMeasurableRec s j) ≤ max #s 2 ^ ℵ₀ := by
    apply mk_biUnion_le_of_le_lift _ B _
    · intro j hj
      exact IH j hj (hj.trans_le hi).le
    · rw [lift_power, lift_aleph0]
      rw [← Ordinal.lift_le.{u}, lift_omega, Ordinal.lift_one, ← ord_aleph] at hi
      have H := card_le_of_le_ord hi
      rw [← Ordinal.lift_card] at H
      apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _
      rw [lift_max, Cardinal.lift_ofNat]
      exact le_max_right _ _