How to use `ZFSet.omega`?

Stream: new members

[Bbbbbbbbba]

I want to prove something like:

import Mathlib

example (z : ZFSet) : z ∈ ZFSet.omega → z = ∅ ∨ ∃ y ∈ ZFSet.omega, insert y y = z := sorry

[Ruben Van de Velde]

Why?

[Bbbbbbbbba]

My original goal was to prove that some alternative definitions of omega are equivalent

[Bbbbbbbbba]

But I find it hard to use the hypothesis z ∈ ZFSet.omega

[Bbbbbbbbba]

ZFSet.omega_zero and ZFSet.omega_succ only says that omega is an inductive set, but not that it is the minimal one

[Miyahara Kō]

I'm proving now...

[Mirek Olšák]

example (z : ZFSet) : z ∈ ZFSet.omega → z = ∅ ∨ ∃ y ∈ ZFSet.omega, insert y y = z := by
  intro zin
  obtain ⟨z⟩ := z
  apply ZFSet.mk_mem_iff.mp at zin
  obtain ⟨⟨n⟩, hn⟩ := zin
  simp [PSet.omega] at hn
  cases n with
  | zero =>
    left
    apply Quot.sound
    convert hn
  | succ n =>
    right
    use .mk <| PSet.omega.Func ⟨n⟩
    constructor
    · use ⟨n⟩
    · simp [PSet.ofNat] at hn
      symm
      apply Quot.sound
      convert hn

[Mirek Olšák]

But my proof was very low-level, not sure if there is more convenient way of handling PSet & ZFSet.

[Bbbbbbbbba]

Thanks, I will probably learn quite a few tactic proof techniques from this

[Bbbbbbbbba]

I think ideally Mathlib should (re-)define everything ZF-related in a ZF-only language, so that ordinary users do not need to handle PSet directly.

[Mirek Olšák]

I think people should not use the ZFC universe much, and in the rare cases we want to embed Lean into it, there should be a meta-code to do that.

[Mirek Olšák]

Although that would be a more long-term project...

[Miyahara Kō]

Oh no proof was already done, here is my structured proof:

@[induction_eliminator]
protected lemma ZFSet.ind {motive : ZFSet.{u} → Prop} :
    (mk : ∀ s, motive (mk s)) → ∀ s, motive s :=
  Quotient.ind

@[simp]
lemma ZFSet.insert_mk (s t : PSet.{u}) : insert (mk s) (mk t) = mk (insert s t) :=
  rfl

lemma ZFSet.forall {p : ZFSet.{u} → Prop} : (∀ s, p s) ↔ ∀ s, p (mk s) :=
  Quotient.forall

lemma PSet.mem_omega {s : PSet.{u}} : s ∈ PSet.omega ↔ ∃ n, s.Equiv (ofNat.{u} n) := by
  conv_lhs => simp [PSet.omega, PSet.mem_def]

lemma PSet.omega_subset (N : PSet.{u}) (hN0 : ∅ ∈ N) (hNs : ∀ ⦃n⦄, n ∈ N → insert n n ∈ N) :
    omega ⊆ N := by
  simp only [subset_iff, mem_omega, forall_exists_index]
  intro s n hs
  rw [Mem.congr_left hs]
  clear s hs
  induction n <;> unfold ofNat <;> solve_by_elim

lemma ZFSet.omega_subset (N : ZFSet.{u}) (hN0 : ∅ ∈ N) (hNs : ∀ ⦃n⦄, n ∈ N → insert n n ∈ N) :
    omega ⊆ N := by
  induction N with
  | mk N =>
    rw [omega, subset_iff]
    refine PSet.omega_subset N hN0 ?_
    simpa [ZFSet.forall] using hNs

example ⦃s : ZFSet.{u}⦄ (hs : s ∈ ZFSet.omega) : s = ∅ ∨ ∃ t ∈ ZFSet.omega, insert t t = s := by
  classical
  suffices ZFSet.omega ⊆ insert ∅ (ZFSet.image (fun t => insert t t) ZFSet.omega) by
    revert s hs
    simpa [ZFSet.subset_def] using this
  apply ZFSet.omega_subset
  case hN0 => simp
  intro n hn
  rw [ZFSet.mem_insert_iff, ZFSet.mem_image] at hn ⊢
  replace hn : n ∈ ZFSet.omega := by
    obtain rfl | ⟨n, hn, rfl⟩ := hn <;> solve_by_elim [ZFSet.omega_zero, ZFSet.omega_succ]
  grind only

[Vlad]

import Mathlib

example : ∀ z, z ∈ ZFSet.omega → z = ∅ ∨ ∃ y ∈ ZFSet.omega, insert y y = z := by
  rintro ⟨⟩ ⟨_ | n, h⟩ <;> have h := Quot.sound h; use .inl h
  right; use .mk $ .ofNat n, ⟨_, by rfl⟩, h.symm

[Dexin Zhang]

#34092 provides some better API