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

State before:
n m : Nat
⊢ le n n
Tactic:
show ∃ k, n + k ≃ n
State after:
n m : Nat
⊢ ∃ k, n + k ≃ n

State before:
n m : Nat
⊢ ∃ k, n + k ≃ n
Tactic:
have : n + 0 ≃ n := AA.identR
State after:
n m : Nat
this : n + 0 ≃ n
⊢ ∃ k, n + k ≃ n

State before:
n m : Nat
this : n + 0 ≃ n
⊢ ∃ k, n + k ≃ n
Tactic:
exact Exists.intro 0 ‹n + 0 ≃ n›
State after:
no goals

State before:
n m m' : Nat
a✝ : n ≤ m'
⊢ le n m'.succ
Tactic:
show le n (step m')
State after:
n m m' : Nat
a✝ : n ≤ m'
⊢ le n (step m')

State before:
n m m' : Nat
a✝ : n ≤ m'
⊢ le n (step m')
Tactic:
have : le n m' := impl_le_from_prelude_le ‹n ≤ m'›
State after:
n m m' : Nat
a✝ : n ≤ m'
this : le n m'
⊢ le n (step m')

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

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

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

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

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