Theorem: Nat.recComplete_eq (Algdata/Data/Nat/Rec.lean)

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
⊢ recComplete ind n = recCompleteWF ind n
Tactic:
suffices ∀ k (hk : k ≤ n), recComplete.aux (motive:=motive) ind n k hk = recCompleteWF (motive:=motive) ind k
  from this n n.le_refl
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
⊢ ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
⊢ ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
Tactic:
intro k hk
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n k : Nat
hk : k ≤ n
⊢ recComplete.aux ind n k hk = recCompleteWF ind k

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n k : Nat
hk : k ≤ n
⊢ recComplete.aux ind n k hk = recCompleteWF ind k
Tactic:
induction n generalizing k
State after:
case zero
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ recComplete.aux ind zero k hk = recCompleteWF ind k

case succ
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n✝ : Nat
n_ih✝ : ∀ (k : Nat) (hk : k ≤ n✝), recComplete.aux ind n✝ k hk = recCompleteWF ind k
k : Nat
hk : k ≤ succ n✝
⊢ recComplete.aux ind (succ n✝) k hk = recCompleteWF ind k

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ recComplete.aux ind zero k hk = recCompleteWF ind k
Tactic:
case zero =>
  dsimp [recComplete.aux]; unfold recCompleteWF
  have : k = 0 := k.eq_zero_of_le_zero hk
  cases this
  apply congrArg; funext k hk; cases hk
State after:
no goals

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : k ≤ succ n
⊢ recComplete.aux ind (succ n) k hk = recCompleteWF ind k
Tactic:
case succ n h_ind =>
  cases k
  case zero =>
    dsimp [recComplete.aux]; unfold recCompleteWF
    apply congrArg; funext k hk; cases hk
  case succ k =>
    dsimp [recComplete.aux]; unfold recCompleteWF
    apply congrArg; funext k hk; rw [h_ind]
State after:
no goals

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ recComplete.aux ind zero k hk = recCompleteWF ind k
Tactic:
dsimp [recComplete.aux]
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = recCompleteWF ind k

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = recCompleteWF ind k
Tactic:
unfold recCompleteWF
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1
Tactic:
have : k = 0 := k.eq_zero_of_le_zero hk
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
this : k = 0
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
this : k = 0
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1
Tactic:
cases this
State after:
case refl
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (ind 0 fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind 0 fun k x => recCompleteWF ind k

State before:
case refl
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (ind 0 fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind 0 fun k x => recCompleteWF ind k
Tactic:
apply congrArg
State after:
case refl.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = fun k x => recCompleteWF ind k

State before:
case refl.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = fun k x => recCompleteWF ind k
Tactic:
funext k hk
State after:
case refl.h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk✝ : 0 ≤ zero
k : Nat
hk : k < 0
⊢ absurd (_ : k < 0) (_ : ¬k < 0) = recCompleteWF ind k

State before:
case refl.h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk✝ : 0 ≤ zero
k : Nat
hk : k < 0
⊢ absurd (_ : k < 0) (_ : ¬k < 0) = recCompleteWF ind k
Tactic:
cases hk
State after:
no goals

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : k ≤ succ n
⊢ recComplete.aux ind (succ n) k hk = recCompleteWF ind k
Tactic:
cases k
State after:
case zero
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ recComplete.aux ind (succ n) zero hk = recCompleteWF ind zero

case succ
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
n✝ : Nat
hk : succ n✝ ≤ succ n
⊢ recComplete.aux ind (succ n) (succ n✝) hk = recCompleteWF ind (succ n✝)

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ recComplete.aux ind (succ n) zero hk = recCompleteWF ind zero
Tactic:
case zero =>
  dsimp [recComplete.aux]; unfold recCompleteWF
  apply congrArg; funext k hk; cases hk
State after:
no goals

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ recComplete.aux ind (succ n) (succ k) hk = recCompleteWF ind (succ k)
Tactic:
case succ k =>
  dsimp [recComplete.aux]; unfold recCompleteWF
  apply congrArg; funext k hk; rw [h_ind]
State after:
no goals

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ recComplete.aux ind (succ n) zero hk = recCompleteWF ind zero
Tactic:
dsimp [recComplete.aux]
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = recCompleteWF ind 0

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = recCompleteWF ind 0
Tactic:
unfold recCompleteWF
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = ind 0 fun k x => recCompleteWF ind k

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = ind 0 fun k x => recCompleteWF ind k
Tactic:
apply congrArg
State after:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (fun k hk => absurd hk (_ : ¬k < 0)) = fun k x => recCompleteWF ind k

State before:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (fun k hk => absurd hk (_ : ¬k < 0)) = fun k x => recCompleteWF ind k
Tactic:
funext k hk
State after:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk✝ : zero ≤ succ n
k : Nat
hk : k < 0
⊢ absurd hk (_ : ¬k < 0) = recCompleteWF ind k

State before:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk✝ : zero ≤ succ n
k : Nat
hk : k < 0
⊢ absurd hk (_ : ¬k < 0) = recCompleteWF ind k
Tactic:
cases hk
State after:
no goals

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ recComplete.aux ind (succ n) (succ k) hk = recCompleteWF ind (succ k)
Tactic:
dsimp [recComplete.aux]
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = recCompleteWF ind (succ k)

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = recCompleteWF ind (succ k)
Tactic:
unfold recCompleteWF
State after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = ind (succ k) fun k_1 x => recCompleteWF ind k_1

State before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = ind (succ k) fun k_1 x => recCompleteWF ind k_1
Tactic:
apply congrArg
State after:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = fun k_1 x => recCompleteWF ind k_1

State before:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = fun k_1 x => recCompleteWF ind k_1
Tactic:
funext k hk
State after:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k✝ : Nat
hk✝ : succ k✝ ≤ succ n
k : Nat
hk : k < k✝ + 1
⊢ recComplete.aux ind n k (_ : k ≤ n) = recCompleteWF ind k

State before:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k✝ : Nat
hk✝ : succ k✝ ≤ succ n
k : Nat
hk : k < k✝ + 1
⊢ recComplete.aux ind n k (_ : k ≤ n) = recCompleteWF ind k
Tactic:
rw [h_ind]
State after:
no goals