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

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

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

State before:
n m : Nat
⊢ compare n m = Ordering.gt → lt m n
Tactic:
case mp =>
  intro (h : compare n m = Ordering.gt)
  show lt m n
  simp [compare, Ord.compare, compareOfLessAndEq] at h
  split at h
  case isTrue =>
    have : n < m := by assumption
    contradiction
  case isFalse =>
    split at h
    case isTrue =>
      have : n = m := by assumption
      contradiction
    case isFalse =>
      have : ¬(n < m) := by assumption
      have : ¬(n = m) := by assumption
      have : n > m ∨ n ≤ m := Nat.lt_or_ge m n
      match ‹n > m ∨ n ≤ m› with
      | Or.inl (_ : n > m) =>
        have : m < n := ‹n > m›
        have : lt m n := prelude_lt_iff_impl_lt.mp ‹m < n›
        exact this
      | Or.inr (_ : n ≤ m) =>
        have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
        match ‹n = m ∨ n < m› with
        | Or.inl (_ : n = m) =>
          exact absurd ‹n = m› ‹¬(n = m)›
        | Or.inr (_ : n < m) =>
          exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
⊢ lt m n → compare n m = Ordering.gt
Tactic:
case mpr =>
  intro (_ : lt m n)
  show compare n m = Ordering.gt
  have notTwo : ¬ AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
    (trichotomy (order_inst := order) n m).atMostOne
  simp [compare, Ord.compare, compareOfLessAndEq]
  split
  case isTrue =>
    have : n < m := by assumption
    show False
    have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
    have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
      AA.TwoOfThree.oneAndThree ‹lt n m› ‹lt m n›
    exact absurd two notTwo
  case isFalse =>
    split
    case isTrue =>
      have : n = m := by assumption
      show False
      have : n ≃ m := ‹n = m›
      have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
        AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹lt m n›
      exact absurd two notTwo
    case isFalse =>
      show Ordering.gt = Ordering.gt
      rfl
State after:
no goals

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

State before:
n m : Nat
h : compare n m = Ordering.gt
⊢ lt m n
Tactic:
simp [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.gt
⊢ lt m n

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

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

State before:
n m : Nat
h✝ : n < m
h : False
⊢ lt m n
Tactic:
case isTrue =>
  have : n < m := by assumption
  contradiction
State after:
no goals

State before:
n m : Nat
h✝ : ¬n < m
h : (if n = m then Ordering.eq else Ordering.gt) = Ordering.gt
⊢ lt m n
Tactic:
case isFalse =>
  split at h
  case isTrue =>
    have : n = m := by assumption
    contradiction
  case isFalse =>
    have : ¬(n < m) := by assumption
    have : ¬(n = m) := by assumption
    have : n > m ∨ n ≤ m := Nat.lt_or_ge m n
    match ‹n > m ∨ n ≤ m› with
    | Or.inl (_ : n > m) =>
      have : m < n := ‹n > m›
      have : lt m n := prelude_lt_iff_impl_lt.mp ‹m < n›
      exact this
    | Or.inr (_ : n ≤ m) =>
      have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
      match ‹n = m ∨ n < m› with
      | Or.inl (_ : n = m) =>
        exact absurd ‹n = m› ‹¬(n = m)›
      | Or.inr (_ : n < m) =>
        exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
h✝ : n < m
h : False
⊢ lt m n
Tactic:
have : n < m := by assumption
State after:
n m : Nat
h✝ : n < m
h : False
this : n < m
⊢ lt m n

State before:
n m : Nat
h✝ : n < m
h : False
this : n < m
⊢ lt m n
Tactic:
contradiction
State after:
no goals

State before:
n m : Nat
h✝ : n < m
h : False
⊢ n < m
Tactic:
assumption
State after:
no goals

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

case isFalse
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
⊢ lt m n

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
⊢ lt m n
Tactic:
case isTrue =>
  have : n = m := by assumption
  contradiction
State after:
no goals

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
⊢ lt m n
Tactic:
case isFalse =>
  have : ¬(n < m) := by assumption
  have : ¬(n = m) := by assumption
  have : n > m ∨ n ≤ m := Nat.lt_or_ge m n
  match ‹n > m ∨ n ≤ m› with
  | Or.inl (_ : n > m) =>
    have : m < n := ‹n > m›
    have : lt m n := prelude_lt_iff_impl_lt.mp ‹m < n›
    exact this
  | Or.inr (_ : n ≤ m) =>
    have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
    match ‹n = m ∨ n < m› with
    | Or.inl (_ : n = m) =>
      exact absurd ‹n = m› ‹¬(n = m)›
    | Or.inr (_ : n < m) =>
      exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
⊢ lt m n
Tactic:
have : n = m := by assumption
State after:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
this : n = m
⊢ lt m n

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
this : n = m
⊢ lt m n
Tactic:
contradiction
State after:
no goals

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
⊢ n = m
Tactic:
assumption
State after:
no goals

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

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

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝ : ¬n < m
this : ¬n = m
⊢ lt m n
Tactic:
have : n > m ∨ n ≤ m := Nat.lt_or_ge m n
State after:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝¹ : ¬n < m
this✝ : ¬n = m
this : n > m ∨ n ≤ m
⊢ lt m n

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝¹ : ¬n < m
this✝ : ¬n = m
this : n > m ∨ n ≤ m
⊢ lt m n
Tactic:
match ‹n > m ∨ n ≤ m› with
| Or.inl (_ : n > m) =>
  have : m < n := ‹n > m›
  have : lt m n := prelude_lt_iff_impl_lt.mp ‹m < n›
  exact this
| Or.inr (_ : n ≤ m) =>
  have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
  match ‹n = m ∨ n < m› with
  | Or.inl (_ : n = m) =>
    exact absurd ‹n = m› ‹¬(n = m)›
  | Or.inr (_ : n < m) =>
    exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
⊢ ¬n < m
Tactic:
assumption
State after:
no goals

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this : ¬n < m
⊢ ¬n = m
Tactic:
assumption
State after:
no goals

State before:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝¹ : ¬n < m
this✝ : ¬n = m
this : n > m ∨ n ≤ m
h✝ : n > m
⊢ lt m n
Tactic:
have : m < n := ‹n > m›
State after:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝² : ¬n < m
this✝¹ : ¬n = m
this✝ : n > m ∨ n ≤ m
h✝ : n > m
this : m < n
⊢ lt m n

State before:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝² : ¬n < m
this✝¹ : ¬n = m
this✝ : n > m ∨ n ≤ m
h✝ : n > m
this : m < n
⊢ lt m n
Tactic:
have : lt m n := prelude_lt_iff_impl_lt.mp ‹m < n›
State after:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝³ : ¬n < m
this✝² : ¬n = m
this✝¹ : n > m ∨ n ≤ m
h✝ : n > m
this✝ : m < n
this : lt m n
⊢ lt m n

State before:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝³ : ¬n < m
this✝² : ¬n = m
this✝¹ : n > m ∨ n ≤ m
h✝ : n > m
this✝ : m < n
this : lt m n
⊢ lt m n
Tactic:
exact this
State after:
no goals

State before:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝¹ : ¬n < m
this✝ : ¬n = m
this : n > m ∨ n ≤ m
h✝ : n ≤ m
⊢ lt m n
Tactic:
have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
State after:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝² : ¬n < m
this✝¹ : ¬n = m
this✝ : n > m ∨ n ≤ m
h✝ : n ≤ m
this : n = m ∨ n < m
⊢ lt m n

State before:
n m : Nat
h✝² : ¬n < m
h✝¹ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝² : ¬n < m
this✝¹ : ¬n = m
this✝ : n > m ∨ n ≤ m
h✝ : n ≤ m
this : n = m ∨ n < m
⊢ lt m n
Tactic:
match ‹n = m ∨ n < m› with
| Or.inl (_ : n = m) =>
  exact absurd ‹n = m› ‹¬(n = m)›
| Or.inr (_ : n < m) =>
  exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

State before:
n m : Nat
h✝³ : ¬n < m
h✝² : ¬n = m
h : Ordering.gt = Ordering.gt
this✝² : ¬n < m
this✝¹ : ¬n = m
this✝ : n > m ∨ n ≤ m
h✝¹ : n ≤ m
this : n = m ∨ n < m
h✝ : n = m
⊢ lt m n
Tactic:
exact absurd ‹n = m› ‹¬(n = m)›
State after:
no goals

State before:
n m : Nat
h✝³ : ¬n < m
h✝² : ¬n = m
h : Ordering.gt = Ordering.gt
this✝² : ¬n < m
this✝¹ : ¬n = m
this✝ : n > m ∨ n ≤ m
h✝¹ : n ≤ m
this : n = m ∨ n < m
h✝ : n < m
⊢ lt m n
Tactic:
exact absurd ‹n < m› ‹¬(n < m)›
State after:
no goals

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

State before:
n m : Nat
x✝ : lt m n
⊢ compare n m = Ordering.gt
Tactic:
have notTwo : ¬ AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
  (trichotomy (order_inst := order) n m).atMostOne
State after:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
⊢ compare n m = Ordering.gt

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

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

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

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ : n < m
⊢ False
Tactic:
case isTrue =>
  have : n < m := by assumption
  show False
  have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
  have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
    AA.TwoOfThree.oneAndThree ‹lt n m› ‹lt m n›
  exact absurd two notTwo
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.gt
Tactic:
case isFalse =>
  split
  case isTrue =>
    have : n = m := by assumption
    show False
    have : n ≃ m := ‹n = m›
    have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
      AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹lt m n›
    exact absurd two notTwo
  case isFalse =>
    show Ordering.gt = Ordering.gt
    rfl
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ : n < m
⊢ False
Tactic:
have : n < m := by assumption
State after:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this : n < m
⊢ False

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this : n < m
⊢ False
Tactic:
have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
State after:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this✝ : n < m
this : lt n m
⊢ False

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this✝ : n < m
this : lt n m
⊢ False
Tactic:
have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
  AA.TwoOfThree.oneAndThree ‹lt n m› ‹lt m n›
State after:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this✝ : n < m
this : lt n m
two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
⊢ False

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this✝ : n < m
this : lt n m
two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
⊢ False
Tactic:
exact absurd two notTwo
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ : n < m
⊢ n < m
Tactic:
assumption
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.gt
Tactic:
split
State after:
case isTrue
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : n = m
⊢ False

case isFalse
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : ¬n = m
⊢ Ordering.gt = Ordering.gt

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : n = m
⊢ False
Tactic:
case isTrue =>
  have : n = m := by assumption
  show False
  have : n ≃ m := ‹n = m›
  have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
    AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹lt m n›
  exact absurd two notTwo
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : ¬n = m
⊢ Ordering.gt = Ordering.gt
Tactic:
case isFalse =>
  show Ordering.gt = Ordering.gt
  rfl
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : n = m
⊢ False
Tactic:
have : n = m := by assumption
State after:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ this : n = m
⊢ False

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ this : n = m
⊢ False
Tactic:
have : n ≃ m := ‹n = m›
State after:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ this✝ : n = m
this : n ≃ m
⊢ False

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ this✝ : n = m
this : n ≃ m
⊢ False
Tactic:
have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
  AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹lt m n›
State after:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ this✝ : n = m
this : n ≃ m
two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
⊢ False

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ this✝ : n = m
this : n ≃ m
two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
⊢ False
Tactic:
exact absurd two notTwo
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : n = m
⊢ n = m
Tactic:
assumption
State after:
no goals

State before:
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : ¬n = m
⊢ Ordering.gt = Ordering.gt
Tactic:
rfl
State after:
no goals