Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_le_from_impl_le (Lean4Axiomatic/Natural/Impl/Nat.lean)

State before:
n k : Nat
h✝ : n + k ≃ 0
⊢ n ≤ 0
Tactic:
have (And.intro (_ : n ≃ 0) (_ : k ≃ 0)) := zero_sum_split ‹n + k ≃ 0›
State after:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
⊢ n ≤ 0

State before:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
⊢ n ≤ 0
Tactic:
have : n = 0 := ‹n ≃ 0›
State after:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
this : n = 0
⊢ n ≤ 0

State before:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
this : n = 0
⊢ n ≤ 0
Tactic:
match ‹n = 0› with
| rfl => exact Nat.le.refl
State after:
no goals

State before:
n k : Nat
h✝ : n + k ≃ 0
left✝ : n ≃ 0
right✝ : k ≃ 0
this : n = 0
⊢ n ≤ n
Tactic:
exact Nat.le.refl
State after:
no goals

State before:
n m' : Nat
h✝ : n + 0 ≃ step m'
⊢ n ≤ m'.succ
Tactic:
show n ≤ step m'
State after:
n m' : Nat
h✝ : n + 0 ≃ step m'
⊢ n ≤ step m'

State before:
n m' : Nat
h✝ : n + 0 ≃ step m'
⊢ n ≤ step m'
Tactic:
have : n ≃ step m' := Rel.trans (Rel.symm AA.identR) ‹n + 0 ≃ step m'›
State after:
n m' : Nat
h✝ : n + 0 ≃ step m'
this : n ≃ step m'
⊢ n ≤ step m'

State before:
n m' : Nat
h✝ : n + 0 ≃ step m'
this : n ≃ step m'
⊢ n ≤ step m'
Tactic:
have : n = step m' := ‹n ≃ step m'›
State after:
n m' : Nat
h✝ : n + 0 ≃ step m'
this✝ : n ≃ step m'
this : n = step m'
⊢ n ≤ step m'

State before:
n m' : Nat
h✝ : n + 0 ≃ step m'
this✝ : n ≃ step m'
this : n = step m'
⊢ n ≤ step m'
Tactic:
match ‹n = step m'› with
| rfl => exact Nat.le.refl
State after:
no goals

State before:
n m' : Nat
h✝ : n + 0 ≃ step m'
this✝ : n ≃ step m'
this : n = step m'
⊢ n ≤ n
Tactic:
exact Nat.le.refl
State after:
no goals

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
⊢ n ≤ m'.succ
Tactic:
show n ≤ step m'
State after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
⊢ n ≤ step m'

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
⊢ n ≤ step m'
Tactic:
have : step (n + k') ≃ step m' := calc
  step (n + k') ≃ _ := Rel.symm add_step
  n + step k'   ≃ _ := ‹n + step k' ≃ step m'›
  step m'       ≃ _ := Rel.refl
State after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this : step (n + k') ≃ step m'
⊢ n ≤ step m'

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this : step (n + k') ≃ step m'
⊢ n ≤ step m'
Tactic:
have : n + k' ≃ m' := AA.inject ‹step (n + k') ≃ step m'›
State after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝ : step (n + k') ≃ step m'
this : n + k' ≃ m'
⊢ n ≤ step m'

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝ : step (n + k') ≃ step m'
this : n + k' ≃ m'
⊢ n ≤ step m'
Tactic:
have : ∃ k', n + k' ≃ m' := Exists.intro k' ‹n + k' ≃ m'›
State after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝¹ : step (n + k') ≃ step m'
this✝ : n + k' ≃ m'
this : ∃ k', n + k' ≃ m'
⊢ n ≤ step m'

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝¹ : step (n + k') ≃ step m'
this✝ : n + k' ≃ m'
this : ∃ k', n + k' ≃ m'
⊢ n ≤ step m'
Tactic:
have : le n m' := ‹∃ k', n + k' ≃ m'›
State after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝² : step (n + k') ≃ step m'
this✝¹ : n + k' ≃ m'
this✝ : ∃ k', n + k' ≃ m'
this : le n m'
⊢ n ≤ step m'

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝² : step (n + k') ≃ step m'
this✝¹ : n + k' ≃ m'
this✝ : ∃ k', n + k' ≃ m'
this : le n m'
⊢ n ≤ step m'
Tactic:
have : n ≤ m' := prelude_le_from_impl_le ‹le n m'›
State after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝³ : step (n + k') ≃ step m'
this✝² : n + k' ≃ m'
this✝¹ : ∃ k', n + k' ≃ m'
this✝ : le n m'
this : n ≤ m'
⊢ n ≤ step m'

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝³ : step (n + k') ≃ step m'
this✝² : n + k' ≃ m'
this✝¹ : ∃ k', n + k' ≃ m'
this✝ : le n m'
this : n ≤ m'
⊢ n ≤ step m'
Tactic:
have : n ≤ step m' := Nat.le.step ‹n ≤ m'›
State after:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝⁴ : step (n + k') ≃ step m'
this✝³ : n + k' ≃ m'
this✝² : ∃ k', n + k' ≃ m'
this✝¹ : le n m'
this✝ : n ≤ m'
this : n ≤ step m'
⊢ n ≤ step m'

State before:
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝⁴ : step (n + k') ≃ step m'
this✝³ : n + k' ≃ m'
this✝² : ∃ k', n + k' ≃ m'
this✝¹ : le n m'
this✝ : n ≤ m'
this : n ≤ step m'
⊢ n ≤ step m'
Tactic:
exact this
State after:
no goals