x y : PartENat
⊢ ((∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy) ↔
    ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
x y : PartENat
⊢ x < y ↔ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
rw [lt_iff_le_not_le, le_def, le_def, not_exists]
case mp
x y : PartENat
⊢ ((∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy) →
    ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy

case mpr
x y : PartENat
⊢ (∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy) →
    (∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
x y : PartENat
⊢ ((∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy) ↔
    ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
constructor
case mp.intro.intro
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
case mp
x y : PartENat
⊢ ((∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy) →
    ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
rintro ⟨⟨hyx, H⟩, h⟩
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy

case neg
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
case mp.intro.intro
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
by_cases hx : x.Dom
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
⊢ ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
use hx
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
hy : y.Dom
⊢ Part.get x hx < Part.get y hy
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
⊢ ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
intro hy
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
⊢ Part.get x hx < Part.get y hy
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
hy : y.Dom
⊢ Part.get x hx < Part.get y hy
specialize H hy
case pos
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
h : ¬∀ (hy_1 : x.Dom), Part.get y hy ≤ Part.get x hy_1
⊢ Part.get x hx < Part.get y hy
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
⊢ Part.get x hx < Part.get y hy
specialize h fun _ => hy
case pos
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
h : ∃ x_1, ¬Part.get y hy ≤ Part.get x x_1
⊢ Part.get x hx < Part.get y hy
case pos
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
h : ¬∀ (hy_1 : x.Dom), Part.get y hy ≤ Part.get x hy_1
⊢ Part.get x hx < Part.get y hy
rw [not_forall] at h
case pos.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
hx' : x.Dom
h : ¬Part.get y hy ≤ Part.get x hx'
⊢ Part.get x hx < Part.get y hy
case pos
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
h : ∃ x_1, ¬Part.get y hy ≤ Part.get x x_1
⊢ Part.get x hx < Part.get y hy
cases' h with hx' h
case pos.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
hx' : x.Dom
h : Part.get x hx' < Part.get y hy
⊢ Part.get x hx < Part.get y hy
case pos.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
hx' : x.Dom
h : ¬Part.get y hy ≤ Part.get x hx'
⊢ Part.get x hx < Part.get y hy
rw [not_le] at h
no goals
case pos.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
hx' : x.Dom
h : Part.get x hx' < Part.get y hy
⊢ Part.get x hx < Part.get y hy
exact h
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
h : ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
case neg
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
specialize h fun hx' => (hx hx').elim
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
h : ∃ x_1, ¬Part.get y (_ : y.Dom) ≤ Part.get x x_1
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
h : ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
rw [not_forall] at h
case neg.intro
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
hx' : x.Dom
h : ¬Part.get y (_ : y.Dom) ≤ Part.get x hx'
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
h : ∃ x_1, ¬Part.get y (_ : y.Dom) ≤ Part.get x x_1
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
cases' h with hx' h
no goals
case neg.intro
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
hx' : x.Dom
h : ¬Part.get y (_ : y.Dom) ≤ Part.get x hx'
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
exact (hx hx').elim
case mpr.intro
x y : PartENat
hx : x.Dom
H : ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
⊢ (∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
    ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
case mpr
x y : PartENat
⊢ (∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy) →
    (∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
rintro ⟨hx, H⟩
no goals
case mpr.intro
x y : PartENat
hx : x.Dom
H : ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
⊢ (∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
    ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
exact ⟨⟨fun _ => hx, fun hy => (H hy).le⟩, fun hxy h => not_lt_of_le (h _) (H _)⟩