internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝¹ : m ≃ n
this✝ : m ≤ n
this : step m ≤ step n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
have : m < step n := lt_step_le.mpr ‹step m ≤ step n›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
apply AA.OneOfThree.third
Proof state after:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ step n > m
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ step n > m
Tactic:
exact ‹m < step n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
apply AA.OneOfThree.third
Proof state after:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ step n > m
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ step n > m
Tactic:
show m < step n
Proof state after:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ m < step n
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ m < step n
Tactic:
exact lt_trans ‹m < n› lt_step
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ ¬AA.TwoOfThree (n < m) (n ≃ m) (n > m)
Tactic:
intro
| AA.TwoOfThree.oneAndTwo (_ : n < m) (_ : n ≃ m) =>
  show False
  have ⟨_, (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
  exact absurd ‹n ≃ m› ‹n ≄ m›
| AA.TwoOfThree.oneAndThree (_ : n < m) (_ : n > m) =>
  show False
  have ⟨(_ : n ≤ m), (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
  have ⟨(_ : m ≤ n), _⟩ := lt_defn.mp ‹n > m›
  have : n ≃ m := le_antisymm ‹n ≤ m› ‹m ≤ n›
  exact absurd ‹n ≃ m› ‹n ≄ m›
| AA.TwoOfThree.twoAndThree (_ : n ≃ m) (_ : n > m) =>
  show False
  have ⟨_, (_ : m ≄ n)⟩ := lt_defn.mp ‹n > m›
  exact absurd ‹n ≃ m› (Rel.symm ‹m ≄ n›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
b✝ : n ≃ m
⊢ False
Tactic:
have ⟨_, (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
b✝ : n ≃ m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
b✝ : n ≃ m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False
Tactic:
exact absurd ‹n ≃ m› ‹n ≄ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
⊢ False
Tactic:
have ⟨(_ : n ≤ m), (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False
Tactic:
have ⟨(_ : m ≤ n), _⟩ := lt_defn.mp ‹n > m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False
Tactic:
have : n ≃ m := le_antisymm ‹n ≤ m› ‹m ≤ n›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
this : n ≃ m
⊢ False
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
this : n ≃ m
⊢ False
Tactic:
exact absurd ‹n ≃ m› ‹n ≄ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
c✝ : n > m
⊢ False
Tactic:
have ⟨_, (_ : m ≄ n)⟩ := lt_defn.mp ‹n > m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
c✝ : n > m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
c✝ : n > m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False
Tactic:
exact absurd ‹n ≃ m› (Rel.symm ‹m ≄ n›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have tri : AA.OneOfThree (n < m) (n ≃ m) (n > m) :=
  (trichotomy n m).atLeastOne
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ compare n m = compare (n + k) (m + k)
Tactic:
match tri with
| AA.OneOfThree.first (_ : n < m) =>
  have : compare n m = Ordering.lt := compare_lt.mpr ‹n < m›
  have : n + k < m + k := lt_substL_add ‹n < m›
  have : compare (n + k) (m + k) = Ordering.lt := compare_lt.mpr this
  calc
    compare n m
      = _ := ‹compare n m = Ordering.lt›
    Ordering.lt
      = _ := by rw [‹compare (n + k) (m + k) = Ordering.lt›]
    compare (n + k) (m + k)
      = _ := rfl
| AA.OneOfThree.second (_ : n ≃ m) =>
  have : compare n m = Ordering.eq := compare_eq.mpr ‹n ≃ m›
  have : n + k ≃ m + k := AA.substL ‹n ≃ m›
  have : compare (n + k) (m + k) = Ordering.eq :=
    compare_eq.mpr ‹n + k ≃ m + k›
  calc
    compare n m
      = _ := ‹compare n m = Ordering.eq›
    Ordering.eq
      = _ := Eq.symm ‹compare (n + k) (m + k) = Ordering.eq›
    compare (n + k) (m + k)
      = _ := rfl
| AA.OneOfThree.third (_ : n > m) =>
  have : compare n m = Ordering.gt := compare_gt.mpr ‹n > m›
  have : n + k > m + k := lt_substL_add ‹n > m›
  have : compare (n + k) (m + k) = Ordering.gt :=
    compare_gt.mpr ‹n + k > m + k›
  calc
    compare n m
      = _ := ‹compare n m = Ordering.gt›
    Ordering.gt
      = _ := Eq.symm ‹compare (n + k) (m + k) = Ordering.gt›
    compare (n + k) (m + k)
      = _ := rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : compare n m = Ordering.lt := compare_lt.mpr ‹n < m›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this : compare n m = Ordering.lt
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this : compare n m = Ordering.lt
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : n + k < m + k := lt_substL_add ‹n < m›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝ : compare n m = Ordering.lt
this : n + k < m + k
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝ : compare n m = Ordering.lt
this : n + k < m + k
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : compare (n + k) (m + k) = Ordering.lt := compare_lt.mpr this
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝¹ : compare n m = Ordering.lt
this✝ : n + k < m + k
this : compare (n + k) (m + k) = Ordering.lt
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝¹ : compare n m = Ordering.lt
this✝ : n + k < m + k
this : compare (n + k) (m + k) = Ordering.lt
⊢ compare n m = compare (n + k) (m + k)
Tactic:
calc
  compare n m
    = _ := ‹compare n m = Ordering.lt›
  Ordering.lt
    = _ := by rw [‹compare (n + k) (m + k) = Ordering.lt›]
  compare (n + k) (m + k)
    = _ := rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝¹ : compare n m = Ordering.lt
this✝ : n + k < m + k
this : compare (n + k) (m + k) = Ordering.lt
⊢ Ordering.lt = compare (n + k) (m + k)
Tactic:
rw [‹compare (n + k) (m + k) = Ordering.lt›]
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : compare n m = Ordering.eq := compare_eq.mpr ‹n ≃ m›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this : compare n m = Ordering.eq
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this : compare n m = Ordering.eq
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : n + k ≃ m + k := AA.substL ‹n ≃ m›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝ : compare n m = Ordering.eq
this : n + k ≃ m + k
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝ : compare n m = Ordering.eq
this : n + k ≃ m + k
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : compare (n + k) (m + k) = Ordering.eq :=
  compare_eq.mpr ‹n + k ≃ m + k›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝¹ : compare n m = Ordering.eq
this✝ : n + k ≃ m + k
this : compare (n + k) (m + k) = Ordering.eq
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝¹ : compare n m = Ordering.eq
this✝ : n + k ≃ m + k
this : compare (n + k) (m + k) = Ordering.eq
⊢ compare n m = compare (n + k) (m + k)
Tactic:
calc
  compare n m
    = _ := ‹compare n m = Ordering.eq›
  Ordering.eq
    = _ := Eq.symm ‹compare (n + k) (m + k) = Ordering.eq›
  compare (n + k) (m + k)
    = _ := rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : compare n m = Ordering.gt := compare_gt.mpr ‹n > m›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this : compare n m = Ordering.gt
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this : compare n m = Ordering.gt
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : n + k > m + k := lt_substL_add ‹n > m›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this✝ : compare n m = Ordering.gt
this : n + k > m + k
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this✝ : compare n m = Ordering.gt
this : n + k > m + k
⊢ compare n m = compare (n + k) (m + k)
Tactic:
have : compare (n + k) (m + k) = Ordering.gt :=
  compare_gt.mpr ‹n + k > m + k›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this✝¹ : compare n m = Ordering.gt
this✝ : n + k > m + k
this : compare (n + k) (m + k) = Ordering.gt
⊢ compare n m = compare (n + k) (m + k)
Theorem: Lean4Axiomatic.Natural.compare_add
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this✝¹ : compare n m = Ordering.gt
this✝ : n + k > m + k
this : compare (n + k) (m + k) = Ordering.gt
⊢ compare n m = compare (n + k) (m + k)
Tactic:
calc
  compare n m
    = _ := ‹compare n m = Ordering.gt›
  Ordering.gt
    = _ := Eq.symm ‹compare (n + k) (m + k) = Ordering.gt›
  compare (n + k) (m + k)
    = _ := rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
⊢ compare n m = ord → compare k j = ord → compare (n + k) (m + j) = ord
Tactic:
match ord with
| Ordering.lt =>
  intro (_ : compare n m = Ordering.lt) (_ : compare k j = Ordering.lt)
  show compare (n + k) (m + j) = Ordering.lt
  have : n < m := compare_lt.mp ‹compare n m = Ordering.lt›
  have : k < j := compare_lt.mp ‹compare k j = Ordering.lt›
  have : n + k < m + j := calc
    n + k < m + k := lt_substL_add ‹n < m›
    m + k < m + j := lt_substR_add ‹k < j›
  have : compare (n + k) (m + j) = Ordering.lt := compare_lt.mpr this
  exact this
| Ordering.eq =>
  intro (_ : compare n m = Ordering.eq) (_ : compare k j = Ordering.eq)
  show compare (n + k) (m + j) = Ordering.eq
  have : n ≃ m := compare_eq.mp ‹compare n m = Ordering.eq›
  have : k ≃ j := compare_eq.mp ‹compare k j = Ordering.eq›
  have : n + k ≃ m + j := calc
    n + k ≃ m + k := AA.substL ‹n ≃ m›
    m + k ≃ m + j := AA.substR ‹k ≃ j›
  have : compare (n + k) (m + j) = Ordering.eq := compare_eq.mpr this
  exact this
| Ordering.gt =>
  intro (_ : compare n m = Ordering.gt) (_ : compare k j = Ordering.gt)
  show compare (n + k) (m + j) = Ordering.gt
  have : n > m := compare_gt.mp ‹compare n m = Ordering.gt›
  have : k > j := compare_gt.mp ‹compare k j = Ordering.gt›
  have : m + j < n + k := calc
    m + j < m + k := lt_substR_add ‹j < k›
    m + k < n + k := lt_substL_add ‹m < n›
  have : compare (n + k) (m + j) = Ordering.gt := compare_gt.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
⊢ compare n m = Ordering.lt → compare k j = Ordering.lt → compare (n + k) (m + j) = Ordering.lt
Tactic:
intro (_ : compare n m = Ordering.lt) (_ : compare k j = Ordering.lt)
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
⊢ compare (n + k) (m + j) = Ordering.lt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
⊢ compare (n + k) (m + j) = Ordering.lt
Tactic:
have : n < m := compare_lt.mp ‹compare n m = Ordering.lt›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this : n < m
⊢ compare (n + k) (m + j) = Ordering.lt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this : n < m
⊢ compare (n + k) (m + j) = Ordering.lt
Tactic:
have : k < j := compare_lt.mp ‹compare k j = Ordering.lt›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝ : n < m
this : k < j
⊢ compare (n + k) (m + j) = Ordering.lt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝ : n < m
this : k < j
⊢ compare (n + k) (m + j) = Ordering.lt
Tactic:
have : n + k < m + j := calc
  n + k < m + k := lt_substL_add ‹n < m›
  m + k < m + j := lt_substR_add ‹k < j›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝¹ : n < m
this✝ : k < j
this : n + k < m + j
⊢ compare (n + k) (m + j) = Ordering.lt