internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_eq
Proof state before:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
this : n ≠ m
⊢ False
Tactic:
have : n = m := ‹n ≃ m›
Proof state after:
n m : Nat
x✝ : n ≃ m
h✝¹ : ¬n < m
h✝ : ¬n = m
this✝ : n ≠ m
this : 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
this✝ : n ≠ m
this : n = m
⊢ False
Tactic:
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
⊢ n ≠ m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
⊢ compare n m = Ordering.gt ↔ lt m n
Tactic:
apply Iff.intro
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
⊢ compare n m = Ordering.gt → lt m n
Tactic:
intro (h : compare n m = Ordering.gt)
Proof state after:
n m : Nat
h : compare n m = Ordering.gt
⊢ lt m n
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h : compare n m = Ordering.gt
⊢ lt m n
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.gt
⊢ lt m n
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h✝ : n < m
h : False
⊢ lt m n
Tactic:
case isTrue =>
  have : n < m := by assumption
  contradiction
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h✝ : n < m
h : False
⊢ lt m n
Tactic:
have : n < m := by assumption
Proof state after:
n m : Nat
h✝ : n < m
h : False
this : n < m
⊢ lt m n
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h✝ : n < m
h : False
this : n < m
⊢ lt m n
Tactic:
contradiction
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
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_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
⊢ lt m n
Tactic:
have : n = m := by assumption
Proof state after:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
this : n = m
⊢ lt m n
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : False
this : n = m
⊢ lt m n
Tactic:
contradiction
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
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_gt
Proof 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
Proof state after:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this : ¬n < m
⊢ lt m n
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
⊢ ¬n < m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this : ¬n < m
⊢ ¬n = m
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof state before:
n m : Nat
⊢ lt m n → compare n m = Ordering.gt
Tactic:
intro (_ : lt m n)
Proof state after:
n m : Nat
x✝ : lt m n
⊢ compare n m = Ordering.gt
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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]
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.refl
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ a ≃ a
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ a
Theorem: Lean4Axiomatic.Integer.Impl.Difference.refl
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ a
Tactic:
intro (a₁——a₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.refl
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ a₁——a₂
Tactic:
show a₁ + a₂ ≃ a₁ + a₂
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁ + a₂ ≃ a₁ + a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.refl
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁ + a₂ ≃ a₁ + a₂
Tactic:
exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.symm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a b : Difference ℕ
⊢ a ≃ b → b ≃ a
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ b → b ≃ a
Theorem: Lean4Axiomatic.Integer.Impl.Difference.symm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ b → b ≃ a
Tactic:
intro (a₁——a₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ b → b ≃ a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.symm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ b → b ≃ a₁——a₂
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ ≃ b → b ≃ a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.symm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ ≃ b → b ≃ a₁——a₂
Tactic:
intro (b₁——b₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.symm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ a₁——a₂
Tactic:
intro (_ : a₁ + b₂ ≃ b₁ + a₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
x✝ : a₁ + b₂ ≃ b₁ + a₂
⊢ b₁——b₂ ≃ a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.symm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
x✝ : a₁ + b₂ ≃ b₁ + a₂
⊢ b₁——b₂ ≃ a₁——a₂
Tactic:
show b₁ + a₂ ≃ a₁ + b₂
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
x✝ : a₁ + b₂ ≃ b₁ + a₂
⊢ b₁ + a₂ ≃ a₁ + b₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.symm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
x✝ : a₁ + b₂ ≃ b₁ + a₂
⊢ b₁ + a₂ ≃ a₁ + b₂
Tactic:
exact Rel.symm ‹a₁ + b₂ ≃ b₁ + a₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a b c : Difference ℕ
⊢ a ≃ b → b ≃ c → a ≃ c
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ b → b ≃ c → a ≃ c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ b → b ≃ c → a ≃ c
Tactic:
intro (a₁——a₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ ≃ b → b ≃ c → a₁——a₂ ≃ c
Tactic:
intro (b₁——b₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c
Tactic:
revert c
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ ∀ {c : Difference ℕ}, a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ ∀ {c : Difference ℕ}, a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c → a₁——a₂ ≃ c
Tactic:
intro (c₁——c₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c₁——c₂ → a₁——a₂ ≃ c₁——c₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
⊢ a₁——a₂ ≃ b₁——b₂ → b₁——b₂ ≃ c₁——c₂ → a₁——a₂ ≃ c₁——c₂
Tactic:
intro (_ : a₁ + b₂ ≃ b₁ + a₂) (_ : b₁ + c₂ ≃ c₁ + b₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁——a₂ ≃ c₁——c₂