awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
⊢ Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    (⋃ (n : ℕ), f n)

Tactic:
mem_union_right _ ⟨fun n => ⟨f n, let ⟨j, hj, hf⟩ := hf n; mem_iUnion₂.2 ⟨j, hj, hf⟩⟩, rfl⟩

Premises used: Iff.mpr, MeasurableSpace.generateMeasurableRec, Set.Mem, Membership.mem, Set.mem_union_right, _private.0.MeasurableSpace.iUnion_mem_generateMeasurableRec.match_1, Set.mem_iUnion₂, Subtype.mk, Exists.intro, Set.iUnion, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
⊢ Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    (⋃ (n : ℕ), f n)

Tactic:
exact mem_union_right _ ⟨fun n => ⟨f n, let ⟨j, hj, hf⟩ := hf n; mem_iUnion₂.2 ⟨j, hj, hf⟩⟩, rfl⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
inl : ∀ (h : i ≤ i), x ∈ generateMeasurableRec s i
inr : ∀ (h : i < j), x ∈ generateMeasurableRec s j
⊢ x ∈ generateMeasurableRec s j

Tactic:
rcases h.eq_or_lt with (rfl | h)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i ≤ i
⊢ x ∈ generateMeasurableRec s i

Tactic:
hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i ≤ i
⊢ x ∈ generateMeasurableRec s i

Tactic:
exact hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h_1 : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ ⋃ (n : ℕ), x ∈ generateMeasurableRec s j

Tactic:
iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩

Premises used: And.intro, Exists.intro, MeasurableSpace.iUnion_mem_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h_1 : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
h₁ : x = ⋃ (n : ℕ), x
⊢ x ∈ generateMeasurableRec s j

Tactic:
convert! iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩

Premises used: And.intro, Exists.intro, MeasurableSpace.iUnion_mem_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h_1 : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ (n : ℕ), x

Tactic:
(iUnion_const x).symm

Premises used: Set.iUnion_const, Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h_1 : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ (n : ℕ), x

Tactic:
exact (iUnion_const x).symm

Premises used: Set.iUnion_const, Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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)
suffices : ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t
⊢ t ∈ generateMeasurableRec s i → p t

Tactic:
suffices H : ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t from H i le_rfl t
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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 : Ordinal.{u_1}
apply :
  ∀ (x : Ordinal.{u_1}),
    (∀ y < x, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t) → x ≤ i → ∀ t ∈ generateMeasurableRec s x, p t
⊢ k ≤ i → ∀ t ∈ generateMeasurableRec s k, p t

Tactic:
apply WellFoundedLT.induction k

Premises used: WellFoundedLT.induction
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : 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}
IH : ∀ y < k, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t
hk : k ≤ i
t : Set α
⊢ ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t

Tactic:
replace IH := fun j hj => IH j hj (hj.le.trans hk)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : 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
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
unfold :
  Membership.mem (γ := Set (Set α))
      (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j;
      s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
      t →
    p t
⊢ t ∈ generateMeasurableRec s k → p t

Tactic:
unfold generateMeasurableRec

Premises used: MeasurableSpace.generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : 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
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
ht : t ∈ s
⊢ p t

Tactic:
hs t ht
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : 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
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
ht : t ∈ s
⊢ p t

Tactic:
exact hs t ht
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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
⊢ p ∅

Tactic:
h0
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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
⊢ p ∅

Tactic:
exact h0
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : 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
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
ht : Membership.mem (γ := Set (Set α)) (compl '' ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) t
⊢ ∃ (x : Set α), (∃ (i : Ordinal.{u_1}) (_ : i < k), x ∈ generateMeasurableRec s i) ∧ xᶜ = t

Tactic:
simp_rw [mem_image, mem_iUnion₂] at ht

Premises used: Set.mem_image, Set.mem_iUnion₂
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : 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
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
ht : ∃ (x : Set α), (∃ (i : Ordinal.{u_1}) (_ : i < k), x ∈ generateMeasurableRec s i) ∧ xᶜ = t
inl : ∀ (u : Set α) (j : Ordinal.{u_1}) (hj : j < k) (hj' : u ∈ generateMeasurableRec s j), p uᶜ
⊢ p t

Tactic:
obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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
u : Set α
j : Ordinal.{u_1}
hj : j < k
hj' : u ∈ generateMeasurableRec s j
⊢ p uᶜ

Tactic:
hc u (IH j hj u hj') ⟨j, hj.trans_le hk, hj'⟩

Premises used: LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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
u : Set α
j : Ordinal.{u_1}
hj : j < k
hj' : u ∈ generateMeasurableRec s j
⊢ p uᶜ

Tactic:
exact hc u (IH j hj u hj') ⟨j, hj.trans_le hk, hj'⟩

Premises used: LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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)
inr : ∀ (n : ℕ), p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j
⊢ p
    ((fun (f : ℕ → (↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) : Type u)) ↦
        (⋃ (n : ℕ), (↑(f n) : Set α) : Set α))
      f)

Tactic:
apply hn
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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 : ℕ
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
⊢ p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j

Tactic:
obtain ⟨j, hj, hj'⟩ := mem_iUnion₂.1 (f n).2

Premises used: Set.mem_iUnion₂, Iff.mp, Subtype.property
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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}
left₁ : j < i
right : (↑(f n) : Set α) ∈ generateMeasurableRec s j
⊢ p (↑(f n) : Set α) ∧ ∃ j < i, (↑(f n) : Set α) ∈ generateMeasurableRec s j

Tactic:
use IH j hj _ hj', j, hj.trans_le hk

Premises used: LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
apply :
  generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1) ⊆
    ⋃ (i : Ordinal.{v}), ⋃ (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), generateMeasurableRec s i
⊢ 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'

Premises used: Set.iUnion₂_subset, MeasurableSpace.generateMeasurableRec_mono, HasSubset.Subset.antisymm'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
rw : ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i
⊢ Membership.mem (γ := Set (Set α))
    (⋃ (i : Ordinal.{v}), ⋃ (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), generateMeasurableRec s i) t

Tactic:
rw [mem_iUnion₂]

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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

Tactic:
generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht

Premises used: MeasurableSpace.generateMeasurableRec_induction
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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
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
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i

Tactic:
refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t_1 : Set α
ht_1 : t_1 ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
t : Set α
ht : t ∈ s
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i

Tactic:
⟨0, omega_pos 1, self_subset_generateMeasurableRec s 0 ht⟩

Premises used: MeasurableSpace.self_subset_generateMeasurableRec, Exists.intro, Ordinal.omega_pos, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t_1 : Set α
ht_1 : t_1 ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
t : Set α
ht : t ∈ s
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), t ∈ generateMeasurableRec s i

Tactic:
exact ⟨0, omega_pos 1, self_subset_generateMeasurableRec s 0 ht⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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), ∅ ∈ generateMeasurableRec s i

Tactic:
⟨0, omega_pos 1, empty_mem_generateMeasurableRec s 0⟩

Premises used: MeasurableSpace.empty_mem_generateMeasurableRec, Exists.intro, Ordinal.omega_pos, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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), ∅ ∈ generateMeasurableRec s i

Tactic:
exact ⟨0, omega_pos 1, empty_mem_generateMeasurableRec s 0⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
u : Set α
j : Ordinal.{v}
hj : j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
hj' : u ∈ generateMeasurableRec s j
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), uᶜ ∈ generateMeasurableRec s i

Tactic:
⟨_, (isSuccLimit_omega 1).succ_lt hj,
      compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩

Premises used: Order.lt_succ, Order.IsSuccLimit.succ_lt, Exists.intro, MeasurableSpace.compl_mem_generateMeasurableRec, OfNat.ofNat, Cardinal.isSuccLimit_omega
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec.{u, v} s ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)
u : Set α
j : Ordinal.{v}
hj : j < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
hj' : u ∈ generateMeasurableRec s j
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), uᶜ ∈ generateMeasurableRec s i

Tactic:
exact ⟨_, (isSuccLimit_omega 1).succ_lt hj,
      compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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
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
⊢ ∃ (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

Premises used: And.left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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)
⊢ ∀ (n : ℕ), I n < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 ∧ f n ∈ generateMeasurableRec.{u, v} s (I n)

Tactic:
simp_rw [exists_prop] at hI

Premises used: exists_prop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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

Tactic:
⟨_, 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⟩⟩

Premises used: Ordinal.lift_iSup_add_one_lt_of_lt_cof, Ordinal.lt_iSup_add_one, And.right, And.left, And.intro, Exists.intro, MeasurableSpace.iUnion_mem_generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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)
refine_4 : Cardinal.lift.{v, 0} #ℕ < (Ordinal.lift.{0, v} ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)).cof
⊢ ∃ (i : Ordinal.{v}) (_ : i < (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1), ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i

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⟩⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
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)
⊢ Cardinal.lift.{v, 0} #ℕ < (Ordinal.lift.{0, v} ((ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1)).cof

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
apply :
  ∀ (x : Ordinal.{u_1}),
    (∀ y < x, generateMeasurableRec s y ⊆ {t : Set α | GenerateMeasurable s t}) →
      generateMeasurableRec s x ⊆ {t : Set α | GenerateMeasurable s t}
⊢ generateMeasurableRec s i ⊆ {t : Set α | GenerateMeasurable s t}

Tactic:
apply WellFoundedLT.induction i

Premises used: WellFoundedLT.induction
-- 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:
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

Premises used: Set.Subset, MeasurableSpace.generateMeasurableRec_induction