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

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

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

State before:
n m : Nat
⊢ compare n m = Ordering.eq → n ≃ m
Tactic:
case mp =>
  intro (h : compare n m = Ordering.eq)
  show n ≃ m
  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
      have : n ≃ m := ‹n = m›
      exact this
    case isFalse =>
      have : n ≠ m := by assumption
      contradiction
State after:
no goals

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

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

State before:
n m : Nat
h : compare n m = Ordering.eq
⊢ n ≃ m
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.eq
⊢ 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.eq
⊢ n ≃ m
Tactic:
split at h
State after:
case isTrue
n m : Nat
h✝ : n < m
h : False
⊢ n ≃ m

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

State before:
n m : Nat
h✝ : n < m
h : False
⊢ n ≃ m
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.eq
⊢ n ≃ m
Tactic:
case isFalse =>
  split at h
  case isTrue =>
    have : n = m := by assumption
    have : n ≃ m := ‹n = m›
    exact this
  case isFalse =>
    have : n ≠ m := by assumption
    contradiction
State after:
no goals

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

State before:
n m : Nat
h✝ : n < m
h : False
this : n < m
⊢ n ≃ m
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.eq
⊢ n ≃ m
Tactic:
split at h
State after:
case isTrue
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
⊢ n ≃ m

case isFalse
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : False
⊢ n ≃ m

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
⊢ n ≃ m
Tactic:
case isTrue =>
  have : n = m := by assumption
  have : n ≃ m := ‹n = m›
  exact this
State after:
no goals

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

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
⊢ n ≃ m
Tactic:
have : n = m := by assumption
State after:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
this : n = m
⊢ n ≃ m

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
this : n = m
⊢ n ≃ m
Tactic:
have : n ≃ m := ‹n = m›
State after:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
this✝ : n = m
this : n ≃ m
⊢ n ≃ m

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

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

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

State before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : False
this : n ≠ m
⊢ n ≃ m
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
⊢ n ≃ m → compare n m = Ordering.eq
Tactic:
intro (_ : n ≃ m)
State after:
n m : Nat
x✝ : n ≃ m
⊢ compare n m = Ordering.eq

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

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

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

State before:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
⊢ False
Tactic:
case isTrue =>
  have : n < m := by assumption
  have : n = m := ‹n ≃ m›
  rw [‹n = m›] at ‹n < m›
  have : ¬(m < m) := Nat.lt_irrefl m
  exact absurd ‹m < m› ‹¬(m < m)›
State after:
no goals

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

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

State before:
n m : Nat
x✝ : n ≃ m
h✝ this : n < m
⊢ False
Tactic:
have : n = m := ‹n ≃ m›
State after:
n m : Nat
x✝ : n ≃ m
h✝ this✝ : n < m
this : n = m
⊢ False

State before:
n m : Nat
x✝ : n ≃ m
h✝ this✝ : n < m
this : n = m
⊢ False
Tactic:
rw [‹n = m›] at ‹n < m›
State after:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
this✝ : m < m
this : n = m
⊢ False

State before:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
this✝ : m < m
this : n = m
⊢ False
Tactic:
have : ¬(m < m) := Nat.lt_irrefl m
State after:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
this✝¹ : m < m
this✝ : n = m
this : ¬m < m
⊢ False

State before:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
this✝¹ : m < m
this✝ : n = m
this : ¬m < m
⊢ False
Tactic:
exact absurd ‹m < m› ‹¬(m < m)›
State after:
no goals

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

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

case isFalse
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
⊢ False

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

State before:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
⊢ False
Tactic:
case isFalse =>
  have : n ≠ m := by assumption
  have : n = m := ‹n ≃ m›
  exact absurd ‹n = m› ‹n ≠ m›
State after:
no goals

State before:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : n = m
⊢ Ordering.eq = Ordering.eq
Tactic:
rfl
State after:
no goals

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

State before:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
this : n ≠ m
⊢ False
Tactic:
have : n = m := ‹n ≃ m›
State after:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
this✝ : n ≠ m
this : n = m
⊢ False

State before:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
this✝ : n ≠ m
this : n = m
⊢ False
Tactic:
exact absurd ‹n = m› ‹n ≠ m›
State after:
no goals

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