-- Mathlib/Data/Nat/PartENat.lean
theorem lt_def (x y : PartENat) : x < y ↔ ∃ hx : x.Dom, ∀ hy : y.Dom, x.get hx < y.get hy

Proof state:
case h
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
h : ¬∀ (hy_1 : x.Dom), y.get hy ≤ x.get hy_1
⊢ x.get hx < y.get hy

Tactic:
rw [not_forall] at h

Result:
case h
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
h : ∃ (x_1 : x.Dom), ¬y.get hy ≤ x.get x_1
⊢ x.get hx < y.get hy

Proof state:
case h.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
hx' : x.Dom
h : x.get hx' < y.get hy
⊢ x.get hx < y.get hy

Tactic:
exact h

Result:
no goals

Proof state:
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
⊢ x.get hx < y.get hy

Tactic:
specialize h fun _ => hy

Result:
case h
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
h : ¬∀ (hy_1 : x.Dom), y.get hy ≤ x.get hy_1
⊢ x.get hx < y.get hy

Proof state:
case neg.intro
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
hx' : x.Dom
h : ¬y.get ⋯ ≤ x.get hx'
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
exact (hx hx').elim

Result:
no goals

Proof state:
case h.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
hx' : x.Dom
h : ¬y.get hy ≤ x.get hx'
⊢ x.get hx < y.get hy

Tactic:
rw [not_le] at h

Result:
case h.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
hx' : x.Dom
h : x.get hx' < y.get hy
⊢ x.get hx < y.get hy

Proof state:
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
h : ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
rw [not_forall] at h

Result:
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
h : ∃ (x_1 : x.Dom), ¬y.get ⋯ ≤ x.get x_1
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Proof state:
case mp
x y : PartENat
⊢ ((∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy) →
    ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
rintro ⟨⟨hyx, H⟩, h⟩

Result:
case mp.intro.intro
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Proof state:
x y : PartENat
⊢ x < y ↔ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
rw [lt_iff_le_not_le, le_def, le_def, not_exists]

Result:
x y : PartENat
⊢ ((∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy) ↔
    ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Proof state:
case mpr
x y : PartENat
⊢ (∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy) →
    (∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy

Tactic:
rintro ⟨hx, H⟩

Result:
case mpr.intro
x y : PartENat
hx : x.Dom
H : ∀ (hy : y.Dom), x.get hx < y.get hy
⊢ (∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
    ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy

Proof state:
case h
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
h : ∃ (x_1 : x.Dom), ¬y.get hy ≤ x.get x_1
⊢ x.get hx < y.get hy

Tactic:
obtain ⟨hx', h⟩ := h

Result:
case h.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
hx' : x.Dom
h : ¬y.get hy ≤ x.get hx'
⊢ x.get hx < y.get hy

Proof state:
case mp.intro.intro
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
by_cases hx : x.Dom

Result:
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : x.Dom
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

case neg
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Proof state:
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : x.Dom
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
use hx

Result:
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : x.Dom
⊢ ∀ (hy : y.Dom), x.get hx < y.get hy

Proof state:
x y : PartENat
⊢ ((∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy) ↔
    ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
constructor

Result:
case mp
x y : PartENat
⊢ ((∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy) →
    ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

case mpr
x y : PartENat
⊢ (∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy) →
    (∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy

Proof state:
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : x.Dom
⊢ ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
intro hy

Result:
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : x.Dom
hy : y.Dom
⊢ x.get hx < y.get hy

Proof state:
case neg
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
specialize h fun hx' => (hx hx').elim

Result:
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
h : ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Proof state:
case mpr.intro
x y : PartENat
hx : x.Dom
H : ∀ (hy : y.Dom), x.get hx < y.get hy
⊢ (∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧
    ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy

Tactic:
exact ⟨⟨fun _ => hx, fun hy => (H hy).le⟩, fun hxy h => not_lt_of_le (h _) (H _)⟩

Result:
no goals

Proof state:
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
h : ∃ (x_1 : x.Dom), ¬y.get ⋯ ≤ x.get x_1
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Tactic:
obtain ⟨hx', h⟩ := h

Result:
case neg.intro
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : ¬x.Dom
hx' : x.Dom
h : ¬y.get ⋯ ≤ x.get hx'
⊢ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

Proof state:
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
hx : x.Dom
hy : y.Dom
⊢ x.get hx < y.get hy

Tactic:
specialize H hy

Result:
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : x.get ⋯ ≤ y.get hy
⊢ x.get hx < y.get hy