More concise way to specify an implicit predicate?

Stream: new members

[Bbbbbbbbba]

The following code works, but I do not like that I have to give a name to h0 : p ∅ := empty_subset x in order to specify its type. Is there a more concise way to do this?

import Mathlib

open ZFSet

def is_inducible (x : ZFSet) : Prop := ∀z ∈ x, z = ∅ ∨ ∃y ∈ x, z = insert y y

lemma inducible_induction {x : ZFSet} {p : ZFSet → Prop}
    (hx : is_inducible x) (h0 : p ∅) (h1 : ∀ y ∈ x, p y → p (insert y y)) : ∀ z ∈ x, p z := by
  let x0 := x.sep fun y ↦ ¬p y
  intro z
  by_contra! hz
  refine x0.eq_empty.mp ?_ z (mem_sep.mpr hz)
  by_contra h
  have ⟨z, hz1, hz2⟩ := regularity x0 h
  have ⟨hzx, hzy⟩ := mem_sep.mp hz1
  apply hzy
  rcases hx z hzx with ⟨hz⟩ | ⟨w, hwx, hwz⟩
  · rw [hz]; exact h0
  · rw [hwz]; apply h1 w hwx
    by_contra hwy
    refine (x0 ∩ z).eq_empty.mp hz2 w (mem_inter.mpr ⟨mem_sep.mpr ⟨hwx, hwy⟩, ?_⟩)
    rw [hwz]
    exact mem_insert w w

lemma inducible_is_transitive {x : ZFSet} (hx : is_inducible x) : IsTransitive x := by
  let p := fun y ↦ y ⊆ x
  have h0 : p ∅ := empty_subset x
  apply inducible_induction hx h0
  intro y hyx hy z hz
  rcases mem_insert_iff.mp hz with hz | hz
  · rw [hz]; exact hyx
  · exact hy hz

[Vlad Tsyrklevich]

It is not clear if you're talking about inducible_induction or inducible_is_transitive. Assuming you're talking about inducible_is_transitive you could have done

  have : p ∅ := empty_subset x
  apply inducible_induction hx this

or

  apply inducible_induction (p := p) hx (empty_subset x)

[Bbbbbbbbba]

Oh yeah I'm looking for the second solution. So every time I had trouble specifying an implicit binder, I could have done this?

[Vlad Tsyrklevich]

Yes, also you could have done

  apply @inducible_induction _ p hx (empty_subset x)

[Vlad Tsyrklevich]

Though I think the first form is often more usable in practice, it's nice to know about the second form as well.

[Bbbbbbbbba]

I learned. Thanks!