awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2 ^ ℵ₀)
have rw : Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2) ^ ℵ₀
Tactic: rw [lift_power, lift_aleph0]
-- 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 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2) ^ ℵ₀
have hi₁ : 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
Cleared hypotheses: hi, A, B
-- 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 : 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 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2) ^ ℵ₀
have H : (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
-- 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 : 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 ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2) ^ ℵ₀
have H₁ : Cardinal.lift.{u, v} i.card ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1
Tactic: rw [← Ordinal.lift_card] at H
Cleared hypotheses: H
-- 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 : 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
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2) ^ ℵ₀
have apply : 2 ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2)
Tactic: apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _
-- 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 : 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 ≤ Cardinal.lift.{v, u} (max (#(↑s : Type u)) 2)
have rw : 2 ≤ max (Cardinal.lift.{v, u} #(↑s : Type u)) 2
Tactic: rw [lift_max, Cardinal.lift_ofNat]
-- 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 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have C : #(↑(⋃ (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 _ _
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have rw : #(↑((s ∪ {∅} ∪ compl '' ⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) ∪
          range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
            ⋃ (n : ℕ), (↑(f n) : Set α)) :
      Type u) ≤
  max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: rw [generateMeasurableRec]
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑((s ∪ {∅} ∪ compl '' ⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) ∪
            range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
              ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀
have h1 : #(↑s : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: apply_rules [(mk_union_le _ _).trans, add_le_of_le (aleph_one_le_continuum.trans A),
    mk_image_le.trans]
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h1 : #(↑s : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑((s ∪ {∅} ∪ compl '' ⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) ∪
            range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
              ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀
have h1₁ : #(↑{∅} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: apply_rules [(mk_union_le _ _).trans, add_le_of_le (aleph_one_le_continuum.trans A),
    mk_image_le.trans]
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h1 : #(↑s : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h1₁ : #(↑{∅} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑((s ∪ {∅} ∪ compl '' ⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) ∪
            range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
              ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀
have h2 : #(↑(range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
          ⋃ (n : ℕ), (↑(f n) : Set α)) :
      Type u) ≤
  max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: apply_rules [(mk_union_le _ _).trans, add_le_of_le (aleph_one_le_continuum.trans A),
    mk_image_le.trans]
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑{∅} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have h1 : 1 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: rw [mk_singleton]
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
            ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀
have h2 : #(ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: apply mk_range_le.trans
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : 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 h2 : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: simp only [mk_pi, prod_const, Cardinal.lift_uzero, mk_denumerable, lift_aleph0]
-- 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 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : 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 this : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ (max (#(↑s : Type u)) 2 ^ ℵ₀) ^ ℵ₀
Tactic: have := @power_le_power_right _ _ ℵ₀ C
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
this :
  #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : 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 h2 : ∀
  (this :
    #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : 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 ^ ℵ₀
Tactic: rwa [← power_mul, aleph0_mul_aleph0] at this
Cleared hypotheses: this
-- 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 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
this :
  #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ (max (#(↑s : Type u)) 2 ^ ℵ₀) ^ ℵ₀
h2 :
  ∀
    (this :
      #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : 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 ^ ℵ₀
⊢ #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have h2₁ : ∀
  (this :
    #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : 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 ^ ℵ₀
Tactic: rwa [← power_mul, aleph0_mul_aleph0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
⊢ #(↑{t : Set α | GenerateMeasurable s t} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
have rw : #(↑(generateMeasurableRec s ((ω_ : (a : Ordinal.{0}) → Ordinal.{0}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
Tactic: rw [generateMeasurable_eq_rec.{u, 0}]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
hs : #(↑s : Type u) ≤ 𝔠
⊢ #(↑{t : Set α | GenerateMeasurable s t} : Type u) ≤ 𝔠
have apply : max (#(↑s : Type u)) 2 ^ ℵ₀ ≤ 𝔠
Tactic: apply (cardinal_generateMeasurable_le s).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
hs : #(↑s : Type u) ≤ 𝔠
⊢ max (#(↑s : Type u)) 2 ^ ℵ₀ ≤ 𝔠
have rw : max (#(↑s : Type u)) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
Tactic: rw [← continuum_power_aleph0]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)
have rw : MeasurableSet.{u_2} (α := β) (⋃ y ∈ s, f ⁻¹' {y})
Tactic: rw [← biUnion_preimage_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
⊢ MeasurableSet.{u_2} (α := β) (⋃ y ∈ s, f ⁻¹' {y})
have refine : ∀ (y : α) (hy : y ∈ s), MeasurableSet (f ⁻¹' {y})
Tactic: refine MeasurableSet.iUnion fun y => MeasurableSet.iUnion fun hy => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
y : α
hy : y ∈ s
⊢ MeasurableSet (f ⁻¹' {y})
have pos : ∀ (hyf : y ∈ range f), MeasurableSet (f ⁻¹' {y})
Tactic: by_cases hyf : y ∈ range f
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
y : α
hy : y ∈ s
pos : ∀ (hyf : y ∈ range f), MeasurableSet (f ⁻¹' {y})
⊢ MeasurableSet (f ⁻¹' {y})
have neg : ∀ (hyf : y ∉ range f), MeasurableSet (f ⁻¹' {y})
Tactic: by_cases hyf : y ∈ range f
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∈ range f
⊢ MeasurableSet (f ⁻¹' {y})
have pos : ∀ (y : β) (hy : f y ∈ s), MeasurableSet (f ⁻¹' {f y})
Tactic: rcases hyf with ⟨y, rfl⟩
Cleared hypotheses: y, hy, hyf
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
⊢ Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
have refine : ∀ (h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})) (n : ℕ∞), MeasurableSet (f ⁻¹' {n})
Tactic: refine ⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
⊢ MeasurableSet (f ⁻¹' {⊤})
have top : MeasurableSet.{u_6} (α := α) (⋃ (i : ℕ), f ⁻¹' {some i})ᶜ
Tactic: rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
n : ℕ∞
⊢ MeasurableSet (f ⁻¹' {n})
have top : MeasurableSet (f ⁻¹' {⊤})
Tactic: cases n with
  | top =>
    rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]
    exact .compl <| .iUnion h
  | coe n => exact h n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ Measurable f
have h₁ : ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
Tactic: apply measurable_to_countable'
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {false})
have h₁ : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
Tactic: convert! h.compl
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
have h₁ : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
Tactic: rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
h₁ : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
have h₂ : f ⁻¹' {false} = f ⁻¹' {!true}
Tactic: rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
h₁ : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
h₂ : f ⁻¹' {false} = f ⁻¹' {!true}
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
have h₃ : f ⁻¹' {false} = f ⁻¹' {false}
Tactic: rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
⊢ Measurable f
have refine : ∀ (x : Prop), MeasurableSet (f ⁻¹' {x})
Tactic: refine measurable_to_countable' fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
⊢ MeasurableSet (f ⁻¹' {x})
have pos : ∀ (hx : x), MeasurableSet (f ⁻¹' {x})
Tactic: by_cases hx : x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
pos : ∀ (hx : x), MeasurableSet (f ⁻¹' {x})
⊢ MeasurableSet (f ⁻¹' {x})
have neg : ∀ (hx : ¬x), MeasurableSet (f ⁻¹' {x})
Tactic: by_cases hx : x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
⊢ Measurable (β := ℕ) fun (x : α) ↦ Nat.findGreatest (p x) N
have refine : ∀ (k : ℕ) (hk : k ≤ N), MeasurableSet.{u_1} (α := α) {x : α | Nat.findGreatest (p x) N = k}
Tactic: refine measurable_findGreatest' fun k hk => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet.{u_1} (α := α) {x : α | Nat.findGreatest (p x) N = k}
have simp : MeasurableSet.{u_1} (α := α)
  ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
Tactic: simp only [Nat.findGreatest_eq_iff, setOf_and, setOf_forall, ← compl_setOf]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
have h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
Tactic: apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
have h₃ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
Tactic: apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]