Increasing Sequence of Sets induces Partition on Limit

Stream: new members

[Arshak Parsa]

Can someone prove this?
(Is it even provable?)

import Mathlib

theorem iUnion_eq_iUnion_diff
  {A : ℕ → Set Ω} (hm : Monotone A) (h0 : A 0 = ∅) :
    (⋃ i, A i) = ⋃ i, A i \ A (i - 1) := by
  ext x
  constructor
  · intro h
    simp_all only [Set.mem_iUnion, Set.mem_diff]
    obtain ⟨w, h⟩ := h
    sorry
  · intro h
    simp_all only [Set.mem_iUnion, Set.mem_diff]
    obtain ⟨w, h⟩ := h
    obtain ⟨left, right⟩ := h
    apply Exists.intro
    · exact left

I found a proof here but I don't know how to use Well-Ordering Principle in Lean.

[cairunze cairunze]

Maybe docs#iUnion_disjointed is something you want?
To use WOP, docs#Nat.find, docs#Nat.find_spec etc is useful.

[Arshak Parsa]

I somehow managed to prove this, thanks!

import Mathlib

theorem iUnion_eq_iUnion_diff
  {A : ℕ → Set Ω} (hm : Monotone A) (h0 : A 0 = ∅) :
    (⋃ i, A i) = ⋃ i, A i \ A (i - 1) := by
  ext x
  constructor
  · intro h
    let Nx := {n : ℕ | x ∈ (A n)}
    apply exists_exists_eq_and.mp at h
    obtain ⟨k, h⟩ := h
    have hNx : (Nx).Nonempty := by
      exact Set.nonempty_of_mem h
    let Nx_min := WellFounded.min wellFounded_lt Nx hNx
    have hn : ∀m ∈ Nx, Nx_min≤m := by
      exact fun m a => WellFounded.min_le wellFounded_lt a hNx
    have hNx_min_mem : Nx_min ∈ Nx := by
      exact WellFounded.min_mem wellFounded_lt Nx hNx
    have hz : Nx_min≠0 := by
      aesop
    match Nx_min with
    | 0 => exact False.elim (hz rfl)
    | 1 =>
      aesop
    | k1+2 =>
      set k := k1+2
      have hkm1 : (k-1) ∉ Nx := by
        by_contra hf
        have h1 : k-1 ≤ k → k = k-1 := by
          exact fun a => Nat.le_antisymm (hn (k - 1) (hm (hn (k - 1) hf) hNx_min_mem)) a
        aesop
      have h3 : x ∈ A k := by
        exact hm (hn k hNx_min_mem) hNx_min_mem
      aesop
  · intro h
    simp_all only [Set.mem_iUnion, Set.mem_diff]
    obtain ⟨w, h⟩ := h
    obtain ⟨left, _⟩ := h
    apply Exists.intro
    · exact left

I guess I can also do it with iUnion_disjointed.