Theorem: Lean4Axiomatic.Natural.compare_add (Lean4Axiomatic/Natural/Order.lean)

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
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)

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
State after:
no goals

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›
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)

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›
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)

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
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)

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
State after:
no goals

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›]
State after:
no goals

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›
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)

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›
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)

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›
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)

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
State after:
no goals

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›
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)

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›
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)

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›
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)

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
State after:
no goals