internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
⊢ n < m → lt n m
Tactic:
case mp =>
  intro (_ : n < m)
  show lt n m
  have : step n ≤ m := ‹n < m›
  have : step n ≤ step m := Nat.le_succ_of_le ‹step n ≤ m›
  have : n ≤ m := Nat.le_of_succ_le_succ ‹step n ≤ step m›
  have : le n m := prelude_le_iff_impl_le.mp ‹n ≤ m›
  have : n ≄ m := by
    intro (_ : n ≃ m)
    show False
    have : n = m := ‹n ≃ m›
    rw [‹n = m›] at ‹step n ≤ m›
    have : ¬(step m ≤ m) := Nat.not_succ_le_self m
    exact absurd ‹step m ≤ m› ‹¬(step m ≤ m)›
  have : lt n m := And.intro ‹le n m› ‹n ≄ m›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
⊢ lt n m → n < m
Tactic:
case mpr =>
  intro (_ : lt n m)
  show n < m
  have (And.intro (_ : le n m) (_ : n ≄ m)) := ‹lt n m›
  have : n ≤ m := prelude_le_iff_impl_le.mpr ‹le 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) =>
    have : n ≠ m := ‹n ≄ m›
    exact absurd ‹n = m› ‹n ≠ m›
  | Or.inr (_ : n < m) =>
    exact ‹n < m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
⊢ n < m → lt n m
Tactic:
intro (_ : n < m)
Proof state after:
n m : Nat
x✝ : n < m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
⊢ lt n m
Tactic:
have : step n ≤ m := ‹n < m›
Proof state after:
n m : Nat
x✝ : n < m
this : step n ≤ m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
this : step n ≤ m
⊢ lt n m
Tactic:
have : step n ≤ step m := Nat.le_succ_of_le ‹step n ≤ m›
Proof state after:
n m : Nat
x✝ : n < m
this✝ : step n ≤ m
this : step n ≤ step m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
this✝ : step n ≤ m
this : step n ≤ step m
⊢ lt n m
Tactic:
have : n ≤ m := Nat.le_of_succ_le_succ ‹step n ≤ step m›
Proof state after:
n m : Nat
x✝ : n < m
this✝¹ : step n ≤ m
this✝ : step n ≤ step m
this : n ≤ m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
this✝¹ : step n ≤ m
this✝ : step n ≤ step m
this : n ≤ m
⊢ lt n m
Tactic:
have : le n m := prelude_le_iff_impl_le.mp ‹n ≤ m›
Proof state after:
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ lt n m
Tactic:
have : n ≄ m := by
  intro (_ : n ≃ m)
  show False
  have : n = m := ‹n ≃ m›
  rw [‹n = m›] at ‹step n ≤ m›
  have : ¬(step m ≤ m) := Nat.not_succ_le_self m
  exact absurd ‹step m ≤ m› ‹¬(step m ≤ m)›
Proof state after:
n m : Nat
x✝ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
this : n ≄ m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
this : n ≄ m
⊢ lt n m
Tactic:
have : lt n m := And.intro ‹le n m› ‹n ≄ m›
Proof state after:
n m : Nat
x✝ : n < m
this✝⁴ : step n ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
this✝ : n ≄ m
this : lt n m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
this✝⁴ : step n ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
this✝ : n ≄ m
this : lt n m
⊢ lt n m
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ n ≄ m
Tactic:
intro (_ : n ≃ m)
Proof state after:
n m : Nat
x✝¹ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
x✝ : n ≃ m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝¹ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
x✝ : n ≃ m
⊢ False
Tactic:
have : n = m := ‹n ≃ m›
Proof state after:
n m : Nat
x✝¹ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝¹ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False
Tactic:
rw [‹n = m›] at ‹step n ≤ m›
Proof state after:
n m : Nat
x✝¹ : n < m
this✝³ : step m ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝¹ : n < m
this✝³ : step m ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False
Tactic:
have : ¬(step m ≤ m) := Nat.not_succ_le_self m
Proof state after:
n m : Nat
x✝¹ : n < m
this✝⁴ : step m ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
x✝ : n ≃ m
this✝ : n = m
this : ¬step m ≤ m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝¹ : n < m
this✝⁴ : step m ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
x✝ : n ≃ m
this✝ : n = m
this : ¬step m ≤ m
⊢ False
Tactic:
exact absurd ‹step m ≤ m› ‹¬(step m ≤ m)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
⊢ lt n m → n < m
Tactic:
intro (_ : lt n m)
Proof state after:
n m : Nat
x✝ : lt n m
⊢ n < m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : lt n m
⊢ n < m
Tactic:
have (And.intro (_ : le n m) (_ : n ≄ m)) := ‹lt n m›
Proof state after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
⊢ n < m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
⊢ n < m
Tactic:
have : n ≤ m := prelude_le_iff_impl_le.mpr ‹le n m›
Proof state after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this : n ≤ m
⊢ n < m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this : n ≤ m
⊢ n < m
Tactic:
have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
Proof state after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
⊢ n < m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
⊢ n < m
Tactic:
match ‹n = m ∨ n < m› with
| Or.inl (_ : n = m) =>
  have : n ≠ m := ‹n ≄ m›
  exact absurd ‹n = m› ‹n ≠ m›
| Or.inr (_ : n < m) =>
  exact ‹n < m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
h✝ : n = m
⊢ n < m
Tactic:
have : n ≠ m := ‹n ≄ m›
Proof state after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝¹ : n ≤ m
this✝ : n = m ∨ n < m
h✝ : n = m
this : n ≠ m
⊢ n < m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝¹ : n ≤ m
this✝ : n = m ∨ n < m
h✝ : n = m
this : n ≠ m
⊢ n < m
Tactic:
exact absurd ‹n = m› ‹n ≠ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt
Proof state before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
h✝ : n < m
⊢ n < m
Tactic:
exact ‹n < m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
⊢ compare n m = Ordering.lt ↔ lt n m
Tactic:
apply Iff.intro
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
⊢ compare n m = Ordering.lt → lt n m
Tactic:
intro (h : compare n m = Ordering.lt)
Proof state after:
n m : Nat
h : compare n m = Ordering.lt
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
h : compare n m = Ordering.lt
⊢ lt n m
Tactic:
simp only [compare, Ord.compare, compareOfLessAndEq] at h
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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›
Proof state after:
n m : Nat
h✝ : n < m
h : Ordering.lt = Ordering.lt
this : lt n m
⊢ lt n m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
h✝ : n < m
h : Ordering.lt = Ordering.lt
this : lt n m
⊢ lt n m
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
⊢ lt n m → compare n m = Ordering.lt
Tactic:
intro (_ : lt n m)
Proof state after:
n m : Nat
x✝ : lt n m
⊢ compare n m = Ordering.lt
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
x✝ : lt n m
⊢ compare n m = Ordering.lt
Tactic:
simp only [compare, Ord.compare, compareOfLessAndEq]
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
x✝ : lt n m
h✝ : n < m
⊢ Ordering.lt = Ordering.lt
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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
Proof state after:
n m : Nat
x✝ : lt n m
h✝ this : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.lt
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_lt
Proof state before:
n m : Nat
x✝ : lt n m
h✝ : ¬n < m
⊢ ¬n < m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
⊢ compare n m = Ordering.eq ↔ n ≃ m
Tactic:
apply Iff.intro
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
⊢ compare n m = Ordering.eq → n ≃ m
Tactic:
intro (h : compare n m = Ordering.eq)
Proof state after:
n m : Nat
h : compare n m = Ordering.eq
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h : compare n m = Ordering.eq
⊢ n ≃ m
Tactic:
simp [compare, Ord.compare, compareOfLessAndEq] at h
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝ : n < m
h : False
⊢ n ≃ m
Tactic:
case isTrue =>
  have : n < m := by assumption
  contradiction
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝ : n < m
h : False
⊢ n ≃ m
Tactic:
have : n < m := by assumption
Proof state after:
n m : Nat
h✝ : n < m
h : False
this : n < m
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝ : n < m
h : False
this : n < m
⊢ n ≃ m
Tactic:
contradiction
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝ : n < m
h : False
⊢ n < m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : False
⊢ n ≃ m
Tactic:
case isFalse =>
  have : n ≠ m := by assumption
  contradiction
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
⊢ n ≃ m
Tactic:
have : n = m := by assumption
Proof state after:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
this : n = m
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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›
Proof state after:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
this✝ : n = m
this : n ≃ m
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
⊢ n = m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : False
⊢ n ≃ m
Tactic:
have : n ≠ m := by assumption
Proof state after:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : False
this : n ≠ m
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : False
this : n ≠ m
⊢ n ≃ m
Tactic:
contradiction
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : False
⊢ n ≠ m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
⊢ n ≃ m → compare n m = Ordering.eq
Tactic:
intro (_ : n ≃ m)
Proof state after:
n m : Nat
x✝ : n ≃ m
⊢ compare n m = Ordering.eq
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
⊢ compare n m = Ordering.eq
Tactic:
simp [compare, Ord.compare, compareOfLessAndEq]
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
⊢ False
Tactic:
have : n < m := by assumption
Proof state after:
n m : Nat
x✝ : n ≃ m
h✝ this : n < m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝ this : n < m
⊢ False
Tactic:
have : n = m := ‹n ≃ m›
Proof state after:
n m : Nat
x✝ : n ≃ m
h✝ this✝ : n < m
this : n = m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝ this✝ : n < m
this : n = m
⊢ False
Tactic:
rw [‹n = m›] at ‹n < m›
Proof state after:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
this✝ : m < m
this : n = m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof state after:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
this✝¹ : m < m
this✝ : n = m
this : ¬m < m
⊢ False
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝ : n < m
⊢ n < m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.eq
Tactic:
split
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : n = m
⊢ Ordering.eq = Ordering.eq
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
⊢ False
Tactic:
have : n ≠ m := by assumption
Proof state after:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
this : n ≠ m
⊢ False