Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt (Lean4Axiomatic/Natural/Impl/Nat.lean)

State before:
n m : Nat
⊢ compare n m = Ordering.lt ↔ lt n m
Tactic:
apply Iff.intro
State after:
case mp
n m : Nat
⊢ compare n m = Ordering.lt → lt n m

case mpr
n m : Nat
⊢ lt n m → compare n m = Ordering.lt

State before:
n m : Nat
⊢ compare n m = Ordering.lt → lt n m
Tactic:
case mp =>
  intro (h : compare n m = Ordering.lt)
  show lt n m
  simp only [compare, Ord.compare, compareOfLessAndEq] at h
  split at h
  case isTrue =>
    have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
    exact this
  case isFalse =>
    split at h <;> contradiction
State after:
no goals

State before:
n m : Nat
⊢ lt n m → compare n m = Ordering.lt
Tactic:
case mpr =>
  intro (_ : lt n m)
  show compare n m = Ordering.lt
  simp only [compare, Ord.compare, compareOfLessAndEq]
  split
  case isTrue =>
    show Ordering.lt = Ordering.lt
    rfl
  case isFalse =>
    have : ¬(n < m) := by assumption
    have : n < m := prelude_lt_iff_impl_lt.mpr ‹lt n m›
    exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
⊢ compare n m = Ordering.lt → lt n m
Tactic:
intro (h : compare n m = Ordering.lt)
State after:
n m : Nat
h : compare n m = Ordering.lt
⊢ lt n m

State before:
n m : Nat
h : compare n m = Ordering.lt
⊢ lt n m
Tactic:
simp only [compare, Ord.compare, compareOfLessAndEq] at h
State after:
n m : Nat
h : (if n < m then Ordering.lt else if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
⊢ lt n m

State before:
n m : Nat
h : (if n < m then Ordering.lt else if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
⊢ lt n m
Tactic:
split at h
State after:
case isTrue
n m : Nat
h✝ : n < m
h : Ordering.lt = Ordering.lt
⊢ lt n m

case isFalse
n m : Nat
h✝ : ¬n < m
h : (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
⊢ lt n m

State before:
n m : Nat
h✝ : n < m
h : Ordering.lt = Ordering.lt
⊢ lt n m
Tactic:
case isTrue =>
  have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
  exact this
State after:
no goals

State before:
n m : Nat
h✝ : ¬n < m
h : (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
⊢ lt n m
Tactic:
case isFalse =>
  split at h <;> contradiction
State after:
no goals

State before:
n m : Nat
h✝ : n < m
h : Ordering.lt = Ordering.lt
⊢ lt n m
Tactic:
have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
State after:
n m : Nat
h✝ : n < m
h : Ordering.lt = Ordering.lt
this : lt n m
⊢ lt n m

State before:
n m : Nat
h✝ : n < m
h : Ordering.lt = Ordering.lt
this : lt n m
⊢ lt n m
Tactic:
exact this
State after:
no goals

State before:
n m : Nat
h✝ : ¬n < m
h : (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
⊢ lt n m
Tactic:
split at h <;> contradiction
State after:
no goals

State before:
n m : Nat
⊢ lt n m → compare n m = Ordering.lt
Tactic:
intro (_ : lt n m)
State after:
n m : Nat
x✝ : lt n m
⊢ compare n m = Ordering.lt

State before:
n m : Nat
x✝ : lt n m
⊢ compare n m = Ordering.lt
Tactic:
simp only [compare, Ord.compare, compareOfLessAndEq]
State after:
n m : Nat
x✝ : lt n m
⊢ (if n < m then Ordering.lt else if n = m then Ordering.eq else Ordering.gt) = Ordering.lt

State before:
n m : Nat
x✝ : lt n m
⊢ (if n < m then Ordering.lt else if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
Tactic:
split
State after:
case isTrue
n m : Nat
x✝ : lt n m
h✝ : n < m
⊢ Ordering.lt = Ordering.lt

case isFalse
n m : Nat
x✝ : lt n m
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt

State before:
n m : Nat
x✝ : lt n m
h✝ : n < m
⊢ Ordering.lt = Ordering.lt
Tactic:
case isTrue =>
  show Ordering.lt = Ordering.lt
  rfl
State after:
no goals

State before:
n m : Nat
x✝ : lt n m
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
Tactic:
case isFalse =>
  have : ¬(n < m) := by assumption
  have : n < m := prelude_lt_iff_impl_lt.mpr ‹lt n m›
  exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
x✝ : lt n m
h✝ : n < m
⊢ Ordering.lt = Ordering.lt
Tactic:
rfl
State after:
no goals

State before:
n m : Nat
x✝ : lt n m
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
Tactic:
have : ¬(n < m) := by assumption
State after:
n m : Nat
x✝ : lt n m
h✝ this : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt

State before:
n m : Nat
x✝ : lt n m
h✝ this : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
Tactic:
have : n < m := prelude_lt_iff_impl_lt.mpr ‹lt n m›
State after:
n m : Nat
x✝ : lt n m
h✝ this✝ : ¬n < m
this : n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt

State before:
n m : Nat
x✝ : lt n m
h✝ this✝ : ¬n < m
this : n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
Tactic:
exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
x✝ : lt n m
h✝ : ¬n < m
⊢ ¬n < m
Tactic:
assumption
State after:
no goals