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

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

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

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

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

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

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
this : n + k < m + j
⊢ compare (n + k) (m + j) = Ordering.lt
Tactic:
have : compare (n + k) (m + j) = Ordering.lt := compare_lt.mpr this
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
this : compare (n + k) (m + j) = Ordering.lt
⊢ compare (n + k) (m + j) = Ordering.lt

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
this✝ : n + k < m + j
this : compare (n + k) (m + j) = Ordering.lt
⊢ compare (n + k) (m + j) = Ordering.lt
Tactic:
exact this
State after:
no goals

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.eq → compare k j = Ordering.eq → compare (n + k) (m + j) = Ordering.eq
Tactic:
intro (_ : compare n m = Ordering.eq) (_ : compare k j = Ordering.eq)
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.eq
x✝ : compare k j = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq

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.eq
x✝ : compare k j = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : n ≃ m := compare_eq.mp ‹compare n m = Ordering.eq›
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.eq
x✝ : compare k j = Ordering.eq
this : n ≃ m
⊢ compare (n + k) (m + j) = Ordering.eq

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.eq
x✝ : compare k j = Ordering.eq
this : n ≃ m
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : k ≃ j := compare_eq.mp ‹compare k j = Ordering.eq›
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.eq
x✝ : compare k j = Ordering.eq
this✝ : n ≃ m
this : k ≃ j
⊢ compare (n + k) (m + j) = Ordering.eq

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.eq
x✝ : compare k j = Ordering.eq
this✝ : n ≃ m
this : k ≃ j
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : n + k ≃ m + j := calc
  n + k ≃ m + k := AA.substL ‹n ≃ m›
  m + k ≃ m + j := AA.substR ‹k ≃ j›
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.eq
x✝ : compare k j = Ordering.eq
this✝¹ : n ≃ m
this✝ : k ≃ j
this : n + k ≃ m + j
⊢ compare (n + k) (m + j) = Ordering.eq

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.eq
x✝ : compare k j = Ordering.eq
this✝¹ : n ≃ m
this✝ : k ≃ j
this : n + k ≃ m + j
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : compare (n + k) (m + j) = Ordering.eq := compare_eq.mpr this
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.eq
x✝ : compare k j = Ordering.eq
this✝² : n ≃ m
this✝¹ : k ≃ j
this✝ : n + k ≃ m + j
this : compare (n + k) (m + j) = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq

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.eq
x✝ : compare k j = Ordering.eq
this✝² : n ≃ m
this✝¹ : k ≃ j
this✝ : n + k ≃ m + j
this : compare (n + k) (m + j) = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
exact this
State after:
no goals

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.gt → compare k j = Ordering.gt → compare (n + k) (m + j) = Ordering.gt
Tactic:
intro (_ : compare n m = Ordering.gt) (_ : compare k j = Ordering.gt)
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.gt
x✝ : compare k j = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt

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.gt
x✝ : compare k j = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : n > m := compare_gt.mp ‹compare n m = Ordering.gt›
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.gt
x✝ : compare k j = Ordering.gt
this : n > m
⊢ compare (n + k) (m + j) = Ordering.gt

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.gt
x✝ : compare k j = Ordering.gt
this : n > m
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : k > j := compare_gt.mp ‹compare k j = Ordering.gt›
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.gt
x✝ : compare k j = Ordering.gt
this✝ : n > m
this : k > j
⊢ compare (n + k) (m + j) = Ordering.gt

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.gt
x✝ : compare k j = Ordering.gt
this✝ : n > m
this : k > j
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : m + j < n + k := calc
  m + j < m + k := lt_substR_add ‹j < k›
  m + k < n + k := lt_substL_add ‹m < n›
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.gt
x✝ : compare k j = Ordering.gt
this✝¹ : n > m
this✝ : k > j
this : m + j < n + k
⊢ compare (n + k) (m + j) = Ordering.gt

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.gt
x✝ : compare k j = Ordering.gt
this✝¹ : n > m
this✝ : k > j
this : m + j < n + k
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : compare (n + k) (m + j) = Ordering.gt := compare_gt.mpr this
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.gt
x✝ : compare k j = Ordering.gt
this✝² : n > m
this✝¹ : k > j
this✝ : m + j < n + k
this : compare (n + k) (m + j) = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt

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.gt
x✝ : compare k j = Ordering.gt
this✝² : n > m
this✝¹ : k > j
this✝ : m + j < n + k
this : compare (n + k) (m + j) = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
exact this
State after:
no goals