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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m ↔ step n ≤ m
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m → step n ≤ m

case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ step n ≤ m → n < m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m → step n ≤ m
Tactic:
intro (_ : n < m)
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
⊢ step n ≤ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
⊢ step n ≤ m
Tactic:
have ⟨(_ : n ≤ m), (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ step n ≤ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ step n ≤ m
Tactic:
have ⟨d, (_ : n + d ≃ m)⟩ := le_defn.mp ‹n ≤ m›
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
⊢ step n ≤ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
⊢ step n ≤ m
Tactic:
have : d ≄ 0 := by
  intro (_ : d ≃ 0)
  show False
  apply ‹n ≄ m›
  show n ≃ m
  calc
    n     ≃ _ := Rel.symm add_zero
    n + 0 ≃ _ := AA.substR (Rel.symm ‹d ≃ 0›)
    n + d ≃ _ := ‹n + d ≃ m›
    m     ≃ _ := Rel.refl
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
this : d ≄ 0
⊢ step n ≤ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
this : d ≄ 0
⊢ step n ≤ m
Tactic:
have : Positive d := Signed.positive_defn.mpr ‹d ≄ 0›
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
⊢ step n ≤ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
⊢ step n ≤ m
Tactic:
have ⟨d', (_ : step d' ≃ d)⟩ := positive_step ‹Positive d›
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝¹ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
d' : ℕ
h✝ : step d' ≃ d
⊢ step n ≤ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝¹ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
d' : ℕ
h✝ : step d' ≃ d
⊢ step n ≤ m
Tactic:
apply le_defn.mpr
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝¹ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
d' : ℕ
h✝ : step d' ≃ d
⊢ ∃ k, step n + k ≃ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝¹ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
d' : ℕ
h✝ : step d' ≃ d
⊢ ∃ k, step n + k ≃ m
Tactic:
exists d'
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝¹ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
d' : ℕ
h✝ : step d' ≃ d
⊢ step n + d' ≃ m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝¹ : n + d ≃ m
this✝ : d ≄ 0
this : Positive d
d' : ℕ
h✝ : step d' ≃ d
⊢ step n + d' ≃ m
Tactic:
calc
  step n + d'   ≃ _ := step_add
  step (n + d') ≃ _ := Rel.symm add_step
  n + step d'   ≃ _ := AA.substR ‹step d' ≃ d›
  n + d         ≃ _ := ‹n + d ≃ m›
  m             ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
⊢ d ≄ 0
Tactic:
intro (_ : d ≃ 0)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
x✝ : d ≃ 0
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
x✝ : d ≃ 0
⊢ False
Tactic:
apply ‹n ≄ m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
x✝ : d ≃ 0
⊢ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
d : ℕ
h✝ : n + d ≃ m
x✝ : d ≃ 0
⊢ n ≃ m
Tactic:
calc
  n     ≃ _ := Rel.symm add_zero
  n + 0 ≃ _ := AA.substR (Rel.symm ‹d ≃ 0›)
  n + d ≃ _ := ‹n + d ≃ m›
  m     ≃ _ := Rel.refl
State after:
no goals

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ step n ≤ m → n < m
Tactic:
intro (_ : step n ≤ m)
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
⊢ n < m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
⊢ n < m
Tactic:
have ⟨d, (_ : step n + d ≃ m)⟩ := le_defn.mp ‹step n ≤ m›
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
⊢ n < m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
⊢ n < m
Tactic:
have : n + step d ≃ m := calc
  n + step d   ≃ _ := add_step
  step (n + d) ≃ _ := Rel.symm step_add
  step n + d   ≃ _ := ‹step n + d ≃ m›
  m            ≃ _ := Rel.refl
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this : n + step d ≃ m
⊢ n < m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this : n + step d ≃ m
⊢ n < m
Tactic:
have : ∃ d, n + d ≃ m := ⟨step d, ‹n + step d ≃ m›⟩
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝ : n + step d ≃ m
this : ∃ d, n + d ≃ m
⊢ n < m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝ : n + step d ≃ m
this : ∃ d, n + d ≃ m
⊢ n < m
Tactic:
have : n ≤ m := le_defn.mpr ‹∃ d, n + d ≃ m›
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝¹ : n + step d ≃ m
this✝ : ∃ d, n + d ≃ m
this : n ≤ m
⊢ n < m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝¹ : n + step d ≃ m
this✝ : ∃ d, n + d ≃ m
this : n ≤ m
⊢ n < m
Tactic:
have : n ≄ m := by
  intro (_ : n ≃ m)
  show False
  have : n + step d ≃ n + 0 := calc
    n + step d ≃ _ := ‹n + step d ≃ m›
    m          ≃ _ := Rel.symm ‹n ≃ m›
    n          ≃ _ := Rel.symm add_zero
    n + 0      ≃ _ := Rel.refl
  have : step d ≃ 0 := AA.cancelL ‹n + step d ≃ n + 0›
  exact absurd ‹step d ≃ 0› step_neqv_zero
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
this : n ≄ m
⊢ n < m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
this : n ≄ m
⊢ n < m
Tactic:
apply lt_defn.mpr
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
this : n ≄ m
⊢ n ≤ m ∧ n ≄ m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
this : n ≄ m
⊢ n ≤ m ∧ n ≄ m
Tactic:
exact ⟨‹n ≤ m›, ‹n ≄ m›⟩
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝¹ : n + step d ≃ m
this✝ : ∃ d, n + d ≃ m
this : n ≤ m
⊢ n ≄ m
Tactic:
intro (_ : n ≃ m)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝¹ : n + step d ≃ m
this✝ : ∃ d, n + d ≃ m
this : n ≤ m
x✝ : n ≃ m
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝¹ : n + step d ≃ m
this✝ : ∃ d, n + d ≃ m
this : n ≤ m
x✝ : n ≃ m
⊢ False
Tactic:
have : n + step d ≃ n + 0 := calc
  n + step d ≃ _ := ‹n + step d ≃ m›
  m          ≃ _ := Rel.symm ‹n ≃ m›
  n          ≃ _ := Rel.symm add_zero
  n + 0      ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
x✝ : n ≃ m
this : n + step d ≃ n + 0
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
x✝ : n ≃ m
this : n + step d ≃ n + 0
⊢ False
Tactic:
have : step d ≃ 0 := AA.cancelL ‹n + step d ≃ n + 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝³ : n + step d ≃ m
this✝² : ∃ d, n + d ≃ m
this✝¹ : n ≤ m
x✝ : n ≃ m
this✝ : n + step d ≃ n + 0
this : step d ≃ 0
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝³ : n + step d ≃ m
this✝² : ∃ d, n + d ≃ m
this✝¹ : n ≤ m
x✝ : n ≃ m
this✝ : n + step d ≃ n + 0
this : step d ≃ 0
⊢ False
Tactic:
exact absurd ‹step d ≃ 0› step_neqv_zero
State after:
no goals