awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → (↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) : Type u)
⊢ p
    ((fun (f : ℕ → (↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) : Type u)) ↦
        (⋃ (n : ℕ), (↑(f n) : Set α) : Set α))
      f)
have inr : ∀ (n : ℕ), p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j
Tactic: apply hn
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → (↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) : Type u)
n : ℕ
⊢ p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j
have inr : ∀ (j : Ordinal.{u_1}) (hj : j < k) (hj' : (↑(f n) : Set α) ∈ generateMeasurableRec s j),
  p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j
Tactic: obtain ⟨j, hj, hj'⟩ := mem_iUnion₂.1 (f n).2
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → (↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) : Type u)
n : ℕ
j : Ordinal.{u_1}
hj : j < k
hj' : (↑(f n) : Set α) ∈ generateMeasurableRec s j
⊢ p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j
have left : p (↑(f n) : Set α)
Tactic: use IH j hj _ hj', j, hj.trans_le hk
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → (↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) : Type u)
n : ℕ
j : Ordinal.{u_1}
hj : j < k
hj' : (↑(f n) : Set α) ∈ generateMeasurableRec s j
left : p (↑(f n) : Set α)
w : Ordinal.{u_1}
⊢ p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j
have left₁ : j < i
Tactic: use IH j hj _ hj', j, hj.trans_le hk
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
⊢ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1) =
    ⋃ (i : Ordinal.{v}), ⋃ (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), generateMeasurableRec s i
have apply : generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1) ⊆
  ⋃ (i : Ordinal.{v}), ⋃ (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), generateMeasurableRec s i
Tactic: apply (iUnion₂_subset fun i h => generateMeasurableRec_mono s h.le).antisymm'
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
⊢ Membership.mem (γ := Set (Set α))
    (⋃ (i : Ordinal.{v}), ⋃ (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), generateMeasurableRec s i) t
have rw : ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
Tactic: rw [mem_iUnion₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
have refine_1 : ∀ t ∈ s, ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
Tactic: refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
refine_1 :
  ∀ t ∈ s, ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
have refine_2 : ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ∅ ∈ generateMeasurableRec s i
Tactic: refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
refine_1 :
  ∀ t ∈ s, ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
refine_2 : ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ∅ ∈ generateMeasurableRec s i
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
have refine_3 : ∀ (u : Set α),
  (∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), u ∈ generateMeasurableRec s i) →
    (∃ j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, u ∈ generateMeasurableRec s j) →
      ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), uᶜ ∈ generateMeasurableRec s i
Tactic: refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
refine_1 :
  ∀ t ∈ s, ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
refine_2 : ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ∅ ∈ generateMeasurableRec s i
refine_3 :
  ∀ (u : Set α),
    (∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), u ∈ generateMeasurableRec s i) →
      (∃ j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, u ∈ generateMeasurableRec s j) →
        ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), uᶜ ∈ generateMeasurableRec s i
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
have refine_4 : ∀ (f : ℕ → Set α),
  (∀ (n : ℕ),
      (∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), f n ∈ generateMeasurableRec s i) ∧
        ∃ j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, f n ∈ generateMeasurableRec s j) →
    ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i
Tactic: refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
f : ℕ → Set α
H :
  ∀ (n : ℕ),
    (∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), f n ∈ generateMeasurableRec s i) ∧
      ∃ j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, f n ∈ generateMeasurableRec s j
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i
have refine_4 : ∀ (I : (n : ℕ) → Ordinal.{v})
  (hI : ∀ (n : ℕ), ∃ (_ : I n < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), f n ∈ generateMeasurableRec.{u, v} s (I n)),
  ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i
Tactic: choose I hI using fun n => (H n).1
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (hypothesis)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
f : ℕ → Set α
H :
  ∀ (n : ℕ),
    (∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), f n ∈ generateMeasurableRec s i) ∧
      ∃ j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, f n ∈ generateMeasurableRec s j
I : (n : ℕ) → Ordinal.{v}
hI : ∀ (n : ℕ), ∃ (_ : I n < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), f n ∈ generateMeasurableRec.{u, v} s (I n)
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i
have hI₁ : ∀ (n : ℕ), I n < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ∧ f n ∈ generateMeasurableRec.{u, v} s (I n)
Tactic: simp_rw [exists_prop] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
f : ℕ → Set α
H :
  ∀ (n : ℕ),
    (∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), f n ∈ generateMeasurableRec s i) ∧
      ∃ j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, f n ∈ generateMeasurableRec s j
I : (n : ℕ) → Ordinal.{v}
hI : ∀ (n : ℕ), I n < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ∧ f n ∈ generateMeasurableRec.{u, v} s (I n)
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i
have refine_4 : Cardinal.lift.{v, 0} #ℕ < (Ordinal.lift.{0, v} ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)).cof
Tactic: refine ⟨_, Ordinal.lift_iSup_add_one_lt_of_lt_cof ?_ fun n => (hI n).1,
      iUnion_mem_generateMeasurableRec fun n => ⟨_, Ordinal.lt_iSup_add_one I n, (hI n).2⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ generateMeasurableRec s i ⊆ {t : Set α | GenerateMeasurable s t}
have apply : ∀ (x : Ordinal.{u_1}),
  (∀ y < x, generateMeasurableRec s y ⊆ {t : Set α | GenerateMeasurable s t}) →
    generateMeasurableRec s x ⊆ {t : Set α | GenerateMeasurable s t}
Tactic: apply WellFoundedLT.induction i
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
⊢ {t : Set α | GenerateMeasurable s t} = generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have apply : {t : Set α | GenerateMeasurable s t} ⊆ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
Tactic: apply (generateMeasurableRec_subset s _).antisymm'
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (hypothesis)
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)
⊢ uᶜ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have IH₁ : ∃ (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
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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
⊢ uᶜ ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have 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)
Tactic: obtain ⟨i, hi, hi'⟩ := IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (hypothesis)
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)
⊢ ⋃ (i : ℕ), f i ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have IH₁ : ∀ (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
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : Membership.mem (γ := Set (Set α)) {t : Set α | GenerateMeasurable s t} t
⊢ t ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have basic : ∀ (u : Set α) (hu : u ∈ s), u ∈ 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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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)
⊢ t ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have empty : ∅ ∈ 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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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)
⊢ t ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have 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)
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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)
⊢ t ∈ generateMeasurableRec.{u, u_1} s ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1)
have 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)
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ≤ i
⊢ generateMeasurableRec s i = generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
have apply : generateMeasurableRec s i ≤ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
Tactic: apply (generateMeasurableRec_mono s hi).antisymm'
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ≤ i
⊢ generateMeasurableRec s i ≤ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
have rw : generateMeasurableRec s i ≤ {t : Set α | GenerateMeasurable s t}
Tactic: rw [← generateMeasurable_eq_rec]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have inl : ∀ (hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1),
  #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: obtain hi | hi := le_or_gt i ω₁
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have inr : ∀ (hi : (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 < i),
  #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: obtain hi | hi := le_or_gt i ω₁
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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 s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have inr : #(↑(generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: rw [generateMeasurableRec_of_omega_one_le s hi.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have suffices : ∀ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1, #(↑(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
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i_1 i : Ordinal.{v}
⊢ i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 → #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have 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 ^ ℵ₀
Tactic: apply WellFoundedLT.induction i
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (hypothesis)
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
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: have A : 𝔠 ≤ max #s 2 ^ ℵ₀ := power_le_power_right (le_max_right _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (hypothesis)
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 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: have B := aleph0_le_continuum.trans A
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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 ^ ℵ₀
have apply : ∀ j < i, #(↑(generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: apply mk_biUnion_le_of_le_lift _ B _
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
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 ^ ℵ₀
⊢ #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have apply₁ : Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2 ^ ℵ₀)
Tactic: apply mk_biUnion_le_of_le_lift _ B _