Proof: isField ss ∧ isMonoClass ss ↔ isSigmaField ss ?

Stream: new members

[White Chen]

I am a beginner in Lean. I want to formalize an exercise in a book about probability theory. The exercise is almost the same as A field being a sigma field if and only if it's a monotone class. I have completed most of the proof, and I believe my proof strategy is correct. However, there are some key steps that I cannot resolve, especially the parts involving Nat.find and iUnion.

Here is my formalization of the concepts and propositions involved in this exercise:

import Mathlib.Tactic
import Mathlib.Data.Set.Countable
open Set Classical
universe u

def isField {α : Type u} (ss : Set (Set α)) : Prop :=
  ∅ ∈ ss ∧ (∀ A ∈ ss, Aᶜ ∈ ss) ∧ ∀ A ∈ ss, ∀ B ∈ ss, A ∪ B ∈ ss

def isSigmaField {α : Type u} (ss : Set (Set α)) : Prop :=
  ∅ ∈ ss ∧
  (∀ s ∈ ss, sᶜ ∈ ss) ∧
  ∀ f : ℕ → Set α, (∀ i, f i ∈ ss) → ⋃ i, f i ∈ ss

def isMonoClass {α : Type u} (ss : Set (Set α)) : Prop :=
  (∀ f : ℕ → Set α,
    (∀ i, f i ⊂ f (i+1) ∧ f i ∈ ss) → ⋃ i, f i ∈ ss) ∧
  (∀ f : ℕ → Set α,
    (∀ i, f (i+1) ⊂ f i ∧ f i ∈ ss) → ⋂ i, f i ∈ ss)

-- TODO: GOAL!!!
theorem SigmaField_Field_MonoClass_iff {α : Type u} {ss : Set (Set α)}
        : isField ss ∧ isMonoClass ss ↔ isSigmaField ss:= by
  sorry

The proof I have completed so far is as follows:

import Mathlib.Tactic
import Mathlib.Data.Set.Countable
open Set Classical
universe u

def isField {α : Type u} (ss : Set (Set α)) : Prop :=
  ∅ ∈ ss ∧ (∀ A ∈ ss, Aᶜ ∈ ss) ∧ ∀ A ∈ ss, ∀ B ∈ ss, A ∪ B ∈ ss

def isSigmaField {α : Type u} (ss : Set (Set α)) : Prop :=
  ∅ ∈ ss ∧
  (∀ s ∈ ss, sᶜ ∈ ss) ∧
  ∀ f : ℕ → Set α, (∀ i, f i ∈ ss) → ⋃ i, f i ∈ ss

def isMonoClass {α : Type u} (ss : Set (Set α)) : Prop :=
  (∀ f : ℕ → Set α,
    (∀ i, f i ⊂ f (i+1) ∧ f i ∈ ss) → ⋃ i, f i ∈ ss) ∧
  (∀ f : ℕ → Set α,
    (∀ i, f (i+1) ⊂ f i ∧ f i ∈ ss) → ⋂ i, f i ∈ ss)

def g_delta {α : Type u} (f : ℕ → Set α) (N : ℕ) :=
  ∃ j, j ≥ N ∧ ⋃ i ≤ j, f i ⊃ ⋃ i ≤ (j - 1), f i

noncomputable def I {α : Type u} {f : ℕ → Set α}
      (h : ∀ N, g_delta f N) (n : ℕ) : ℕ :=
  match n with
  | 0 => 0
  | n + 1 => Nat.find (h ((I h n)+1))

lemma I_mono_mono {α : Type u} {f : ℕ → Set α}
        {h : ∀ N, g_delta f N}
        : ∀ i, I h i < I h i.succ:= by
        intro i
        simp [I]
        intro m hmIhi hsuccIhiM
        obtain h:= le_trans hsuccIhiM hmIhi
        simp_all only [add_le_iff_nonpos_right, nonpos_iff_eq_zero, one_ne_zero]

lemma I_mono {α : Type u} {f : ℕ → Set α}
        {h : ∀ N, g_delta f N}
        : ∀ i j, i < j → I h i < I h j:= by
        intro i j hih
        induction hih
        · exact I_mono_mono i
        · rename_i m _ IhileIhm
          exact Nat.lt_trans IhileIhm (I_mono_mono m)

def g' {α : Type u} {f : ℕ → Set α}
      (h : ∀ N, g_delta f N)
      (n : ℕ) : Set α := ⋃ i ≤ (I h n), f i

lemma mono_g {α : Type u} {f : ℕ → Set α}
        {h : ∀ N, g_delta f N}
        : ∀ i j : ℕ, i < j → g' h i ⊆ g' h j := by
  rintro i j i_lt_j
  dsimp [g']
  simp
  rintro k k_le_Ihi
  rw [Set.subset_def]
  intro x xfk
  apply Set.mem_iUnion₂.mpr
  have : I h i < I h j := I_mono i j i_lt_j
  exact ⟨k, (by linarith), xfk⟩

lemma mono_g' {α : Type u} {f : ℕ → Set α}
        {h : ∀ N, g_delta f N}
        : ∀ i j : ℕ, i < j → g' h i ⊂ g' h j := by
  rintro i j i_lt_j
  apply ssubset_iff_subset_ne.mpr
  constructor
  · apply mono_g i j i_lt_j
  · sorry


lemma union_of_SigmaField {α : Type u} {ss : Set (Set α)} {A B : Set α}
        (h : A ∈ ss) (h' : B ∈ ss)
        : isSigmaField ss → A ∪ B ∈ ss := by
  rintro ⟨empty, ⟨_, union⟩⟩
  let f : ℕ → Set α := fun n => if n = 0 then A else if n = 1 then B else ∅
  have : ⋃ i, f i = A ∪ B := by
    ext x
    constructor
    · intro xUfi
      simp at xUfi
      rcases xUfi with ⟨w, xfw⟩
      match w with
      | 0 =>
        apply (Set.mem_union x A B).mpr (Or.inl xfw)
      | 1 =>
        apply (Set.mem_union x A B).mpr (Or.inr xfw)
    · intro this
      rcases this with xA | xB
      · simp
        use 0; norm_num; exact xA
      · simp
        use 1; norm_num; exact xB
  have fi_ss : ∀ i, f i ∈ ss := by
    intro i
    match i with
    | 0 => exact h
    | 1 => exact h'
    | Nat.succ (Nat.succ n) =>
      simp; exact empty
  rw [←this]
  exact union f fi_ss

-- TODO: GOAL!!!
theorem SigmaField_Field_MonoClass_iff {α : Type u} {ss : Set (Set α)}
        : isField ss ∧ isMonoClass ss ↔ isSigmaField ss:= by
  constructor
  · rintro ⟨⟨hempty, ⟨hcompl, hfunion⟩⟩, ⟨hiUnion, hiInter⟩⟩
    have empty : ∅ ∈ ss := by exact hempty
    have compl : ∀ s ∈ ss, sᶜ ∈ ss := by exact hcompl
    have union : ∀ f : ℕ → Set α, (∀ i, f i ∈ ss) → ⋃ i, f i ∈ ss := by
      rintro f hfi_ss
      by_cases h: ∀ N, g_delta f N
      · have h' : ⋃ i, g' h i = ⋃ i, f i := by
          sorry
        rw [←h']
        apply hiUnion
        intro i
        apply And.intro
        · show g' h i ⊂ g' h (i + 1)
          apply mono_g'; simp
        · show g' h i ∈ ss
          dsimp [g']
          sorry
      · sorry
    exact ⟨empty, ⟨compl, union⟩⟩
  · rintro ⟨empty, compl, union⟩
    constructor
    · apply And.intro empty
      apply And.intro compl
      rintro A A_ss B B_ss
      apply union_of_SigmaField A_ss B_ss ⟨empty, compl, union⟩
    · constructor
      · rintro f h
        apply union
        intro i
        exact (h i).right
      · rintro f h
        -- Maybe can be solved by Set.compl_iUnion, Set.compl_iInter and `union`, `compl`, `h` in the context ?
        sorry

The sorry parts are where I am stuck.
Any suggestions or even providing a complete/more concise proof are greatly appreciated.