Theorem: Fin.specFun (GMLInit/Data/Fin/Coding.lean)

State before:
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
⊢ ⟨0, isLt✝⟩.decodeFun = x ↔ encodeFun x = ⟨0, isLt✝⟩
Tactic:
constructor
State after:
case mp
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
⊢ ⟨0, isLt✝⟩.decodeFun = x → encodeFun x = ⟨0, isLt✝⟩

case mpr
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
⊢ encodeFun x = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.decodeFun = x

State before:
case mp
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
⊢ ⟨0, isLt✝⟩.decodeFun = x → encodeFun x = ⟨0, isLt✝⟩
Tactic:
intro | rfl => rfl
State after:
no goals

State before:
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
x✝ : ⟨0, isLt✝⟩.decodeFun = x
⊢ encodeFun ⟨0, isLt✝⟩.decodeFun = ⟨0, isLt✝⟩
Tactic:
rfl
State after:
no goals

State before:
case mpr
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
⊢ encodeFun x = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.decodeFun = x
Tactic:
intro
State after:
case mpr
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
a✝ : encodeFun x = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.decodeFun = x

State before:
case mpr
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝ : 0 < n ^ 0
a✝ : encodeFun x = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.decodeFun = x
Tactic:
funext ⟨_,_⟩
State after:
case mpr.h
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝¹ : 0 < n ^ 0
a✝ : encodeFun x = ⟨0, isLt✝¹⟩
val✝ : Nat
isLt✝ : val✝ < 0
⊢ ⟨0, isLt✝¹⟩.decodeFun ⟨val✝, isLt✝⟩ = x ⟨val✝, isLt✝⟩

State before:
case mpr.h
n : Nat
k : Fin (n ^ 0)
x : Fin 0 → Fin n
isLt✝¹ : 0 < n ^ 0
a✝ : encodeFun x = ⟨0, isLt✝¹⟩
val✝ : Nat
isLt✝ : val✝ < 0
⊢ ⟨0, isLt✝¹⟩.decodeFun ⟨val✝, isLt✝⟩ = x ⟨val✝, isLt✝⟩
Tactic:
contradiction
State after:
no goals

State before:
case succ
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
⊢ k.decodeFun = x ↔ encodeFun x = k
Tactic:
have ih1 : decodeFun (encodeFun (fun k => x (succ k))) = fun k => x (succ k) := by rw [ih]
State after:
case succ
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
⊢ k.decodeFun = x ↔ encodeFun x = k

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
⊢ (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
Tactic:
rw [ih]
State after:
no goals

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
⊢ ⟨k, hk⟩.decodeFun = x ↔ encodeFun x = ⟨k, hk⟩
Tactic:
have hnpos : n > 0 := by
  apply Nat.pos_of_nonzero
  intro h
  rw [h] at hk
  contradiction
State after:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
⊢ ⟨k, hk⟩.decodeFun = x ↔ encodeFun x = ⟨k, hk⟩

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
⊢ ⟨k, hk⟩.decodeFun = x ↔ encodeFun x = ⟨k, hk⟩
Tactic:
constructor
State after:
case mp
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
⊢ ⟨k, hk⟩.decodeFun = x → encodeFun x = ⟨k, hk⟩

case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
⊢ encodeFun x = ⟨k, hk⟩ → ⟨k, hk⟩.decodeFun = x

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
⊢ n > 0
Tactic:
apply Nat.pos_of_nonzero
State after:
case a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
⊢ n ≠ 0

State before:
case a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
⊢ n ≠ 0
Tactic:
intro h
State after:
case a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
h : n = 0
⊢ False

State before:
case a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
h : n = 0
⊢ False
Tactic:
rw [h] at hk
State after:
case a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < 0 ^ (m + 1)
h : n = 0
⊢ False

State before:
case a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < 0 ^ (m + 1)
h : n = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case mp
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
⊢ ⟨k, hk⟩.decodeFun = x → encodeFun x = ⟨k, hk⟩
Tactic:
intro h
State after:
case mp
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ encodeFun x = ⟨k, hk⟩

State before:
case mp
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ encodeFun x = ⟨k, hk⟩
Tactic:
unfold encodeFun
State after:
case mp
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ⟨n * ↑(encodeFun fun k => x k.succ) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩

State before:
case mp
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ⟨n * ↑(encodeFun fun k => x k.succ) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
Tactic:
apply Fin.eq
State after:
case mp.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑⟨n * ↑(encodeFun fun k => x k.succ) + ↑(x 0), ⋯⟩ = ↑⟨k, hk⟩

State before:
case mp.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑⟨n * ↑(encodeFun fun k => x k.succ) + ↑(x 0), ⋯⟩ = ↑⟨k, hk⟩
Tactic:
clean
State after:
case mp.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k

State before:
case mp.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
Tactic:
transitivity (n * (k / n) + k % n)
State after:
case mp.a.left
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = n * (k / n) + k % n

case mp.a.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ n * (k / n) + k % n = k

State before:
case mp.a.left
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = n * (k / n) + k % n
Tactic:
congr
State after:
case mp.a.left.e_a.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(encodeFun fun k => x k.succ) = k / n

case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(x 0) = k % n

State before:
case mp.a.left.e_a.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(encodeFun fun k => x k.succ) = k / n
Tactic:
have : k / n < n ^ m := by rw [Nat.div_lt_iff_lt_mul hnpos]; exact hk
State after:
case mp.a.left.e_a.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
this : k / n < n ^ m
⊢ ↑(encodeFun fun k => x k.succ) = k / n

State before:
case mp.a.left.e_a.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
this : k / n < n ^ m
⊢ ↑(encodeFun fun k => x k.succ) = k / n
Tactic:
have : (encodeFun fun k => x (succ k)) = ⟨k / n, this⟩ := by rw [←ih, ←h]; rfl
State after:
case mp.a.left.e_a.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
this✝ : k / n < n ^ m
this : (encodeFun fun k => x k.succ) = ⟨k / n, this✝⟩
⊢ ↑(encodeFun fun k => x k.succ) = k / n

State before:
case mp.a.left.e_a.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
this✝ : k / n < n ^ m
this : (encodeFun fun k => x k.succ) = ⟨k / n, this✝⟩
⊢ ↑(encodeFun fun k => x k.succ) = k / n
Tactic:
erw [this]
State after:
no goals

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ k / n < n ^ m
Tactic:
rw [Nat.div_lt_iff_lt_mul hnpos]
State after:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ k < n ^ m * n

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ k < n ^ m * n
Tactic:
exact hk
State after:
no goals

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
this : k / n < n ^ m
⊢ (encodeFun fun k => x k.succ) = ⟨k / n, this⟩
Tactic:
rw [←ih, ←h]
State after:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
this : k / n < n ^ m
⊢ ⟨k / n, this⟩.decodeFun = fun k_1 => ⟨k, hk⟩.decodeFun k_1.succ

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
this : k / n < n ^ m
⊢ ⟨k / n, this⟩.decodeFun = fun k_1 => ⟨k, hk⟩.decodeFun k_1.succ
Tactic:
rfl
State after:
no goals

State before:
case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(x 0) = k % n
Tactic:
rw [←h]
State after:
case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(⟨k, hk⟩.decodeFun 0) = k % n

State before:
case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(⟨k, hk⟩.decodeFun 0) = k % n
Tactic:
unfold decodeFun
State after:
case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑((let_fun hn := ⋯;
        fun x =>
        match x with
        | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
        | ⟨i.succ, hi⟩ =>
          let_fun h := ⋯;
          ⟨k / n, h⟩.decodeFun ⟨i, ⋯⟩)
        0) =
    k % n

State before:
case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑((let_fun hn := ⋯;
        fun x =>
        match x with
        | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
        | ⟨i.succ, hi⟩ =>
          let_fun h := ⋯;
          ⟨k / n, h⟩.decodeFun ⟨i, ⋯⟩)
        0) =
    k % n
Tactic:
clean
State after:
case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(match 0 with
      | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
      | ⟨i.succ, hi⟩ => ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩) =
    k % n

State before:
case mp.a.left.e_a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ ↑(match 0 with
      | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
      | ⟨i.succ, hi⟩ => ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩) =
    k % n
Tactic:
split
State after:
case mp.a.left.e_a.h_1
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
isLt✝ : 0 < m + 1
heq✝ : 0 = ⟨0, isLt✝⟩
⊢ ↑⟨k % n, ⋯⟩ = k % n

case mp.a.left.e_a.h_2
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : 0 = ⟨i✝.succ, hi✝⟩
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n

State before:
case mp.a.left.e_a.h_1
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
isLt✝ : 0 < m + 1
heq✝ : 0 = ⟨0, isLt✝⟩
⊢ ↑⟨k % n, ⋯⟩ = k % n

case mp.a.left.e_a.h_2
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : 0 = ⟨i✝.succ, hi✝⟩
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n
Tactic:
next => rfl
State after:
case mp.a.left.e_a.h_2
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : 0 = ⟨i✝.succ, hi✝⟩
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n

State before:
case mp.a.left.e_a.h_2
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : 0 = ⟨i✝.succ, hi✝⟩
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n
Tactic:
next heq => injection heq; contradiction
State after:
no goals

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
isLt✝ : 0 < m + 1
heq✝ : 0 = ⟨0, isLt✝⟩
⊢ ↑⟨k % n, ⋯⟩ = k % n
Tactic:
rfl
State after:
no goals

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq : 0 = ⟨i✝.succ, hi✝⟩
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n
Tactic:
injection heq
State after:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
val_eq✝ : 0 % (m + 1) = i✝.succ
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
val_eq✝ : 0 % (m + 1) = i✝.succ
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n
Tactic:
contradiction
State after:
no goals

State before:
case mp.a.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ n * (k / n) + k % n = k
Tactic:
rw [Nat.add_comm]
State after:
case mp.a.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ k % n + n * (k / n) = k

State before:
case mp.a.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨k, hk⟩.decodeFun = x
⊢ k % n + n * (k / n) = k
Tactic:
exact Nat.mod_add_div ..
State after:
no goals

State before:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
⊢ encodeFun x = ⟨k, hk⟩ → ⟨k, hk⟩.decodeFun = x
Tactic:
intro h
State after:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : encodeFun x = ⟨k, hk⟩
⊢ ⟨k, hk⟩.decodeFun = x

State before:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : encodeFun x = ⟨k, hk⟩
⊢ ⟨k, hk⟩.decodeFun = x
Tactic:
unfold encodeFun at h
State after:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨n * ↑(encodeFun fun k => x k.succ) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ ⟨k, hk⟩.decodeFun = x

State before:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ⟨n * ↑(encodeFun fun k => x k.succ) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ ⟨k, hk⟩.decodeFun = x
Tactic:
injection h with h
State after:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
⊢ ⟨k, hk⟩.decodeFun = x

State before:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
⊢ ⟨k, hk⟩.decodeFun = x
Tactic:
unfold decodeFun
State after:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
⊢ (let_fun hn := ⋯;
    fun x =>
    match x with
    | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
    | ⟨i.succ, hi⟩ =>
      let_fun h := ⋯;
      ⟨k / n, h⟩.decodeFun ⟨i, ⋯⟩) =
    x

State before:
case mpr
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
⊢ (let_fun hn := ⋯;
    fun x =>
    match x with
    | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
    | ⟨i.succ, hi⟩ =>
      let_fun h := ⋯;
      ⟨k / n, h⟩.decodeFun ⟨i, ⋯⟩) =
    x
Tactic:
funext ⟨i, hi⟩
State after:
case mpr.h
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
⊢ (let_fun hn := ⋯;
      fun x =>
      match x with
      | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
      | ⟨i.succ, hi⟩ =>
        let_fun h := ⋯;
        ⟨k / n, h⟩.decodeFun ⟨i, ⋯⟩)
      ⟨i, hi⟩ =
    x ⟨i, hi⟩

State before:
case mpr.h
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
⊢ (let_fun hn := ⋯;
      fun x =>
      match x with
      | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
      | ⟨i.succ, hi⟩ =>
        let_fun h := ⋯;
        ⟨k / n, h⟩.decodeFun ⟨i, ⋯⟩)
      ⟨i, hi⟩ =
    x ⟨i, hi⟩
Tactic:
clean
State after:
case mpr.h
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
⊢ (match ⟨i, hi⟩ with
    | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
    | ⟨i.succ, hi⟩ => ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩) =
    x ⟨i, hi⟩

State before:
case mpr.h
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
⊢ (match ⟨i, hi⟩ with
    | ⟨0, isLt⟩ => ⟨k % n, ⋯⟩
    | ⟨i.succ, hi⟩ => ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩) =
    x ⟨i, hi⟩
Tactic:
split
State after:
case mpr.h.h_1
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
x✝ : Fin (m + 1)
isLt✝ : 0 < m + 1
heq✝ : ⟨i, hi⟩ = ⟨0, isLt✝⟩
⊢ ⟨k % n, ⋯⟩ = x ⟨i, hi⟩

case mpr.h.h_2
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : ⟨i, hi⟩ = ⟨i✝.succ, hi✝⟩
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩ = x ⟨i, hi⟩

State before:
case mpr.h.h_1
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
x✝ : Fin (m + 1)
isLt✝ : 0 < m + 1
heq✝ : ⟨i, hi⟩ = ⟨0, isLt✝⟩
⊢ ⟨k % n, ⋯⟩ = x ⟨i, hi⟩

case mpr.h.h_2
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : ⟨i, hi⟩ = ⟨i✝.succ, hi✝⟩
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩ = x ⟨i, hi⟩
Tactic:
next heq =>
  cases heq
  apply Fin.eq
  simp only [←h]
  rw [Nat.add_comm]
  rw [Nat.add_mul_mod_self_left]
  rw [Nat.mod_eq_of_lt (x 0).isLt]
  rfl
State after:
case mpr.h.h_2
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : ⟨i, hi⟩ = ⟨i✝.succ, hi✝⟩
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩ = x ⟨i, hi⟩

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i : Nat
hi : i < m + 1
x✝ : Fin (m + 1)
isLt✝ : 0 < m + 1
heq : ⟨i, hi⟩ = ⟨0, isLt✝⟩
⊢ ⟨k % n, ⋯⟩ = x ⟨i, hi⟩
Tactic:
cases heq
State after:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ⟨k % n, ⋯⟩ = x ⟨0, hi⟩

State before:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ⟨k % n, ⋯⟩ = x ⟨0, hi⟩
Tactic:
apply Fin.eq
State after:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ↑⟨k % n, ⋯⟩ = ↑(x ⟨0, hi⟩)

State before:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ↑⟨k % n, ⋯⟩ = ↑(x ⟨0, hi⟩)
Tactic:
simp only [←h]
State after:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ (n * ↑(encodeFun fun k => x k.succ) + ↑(x 0)) % n = ↑(x ⟨0, hi⟩)

State before:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ (n * ↑(encodeFun fun k => x k.succ) + ↑(x 0)) % n = ↑(x ⟨0, hi⟩)
Tactic:
rw [Nat.add_comm]
State after:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ (↑(x 0) + n * ↑(encodeFun fun k => x k.succ)) % n = ↑(x ⟨0, hi⟩)

State before:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ (↑(x 0) + n * ↑(encodeFun fun k => x k.succ)) % n = ↑(x ⟨0, hi⟩)
Tactic:
rw [Nat.add_mul_mod_self_left]
State after:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ↑(x 0) % n = ↑(x ⟨0, hi⟩)

State before:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ↑(x 0) % n = ↑(x ⟨0, hi⟩)
Tactic:
rw [Nat.mod_eq_of_lt (x 0).isLt]
State after:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ↑(x 0) = ↑(x ⟨0, hi⟩)

State before:
case refl.a
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
isLt✝ hi : 0 < m + 1
⊢ ↑(x 0) = ↑(x ⟨0, hi⟩)
Tactic:
rfl
State after:
no goals

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i✝ : Nat
hi : i✝ < m + 1
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
heq : ⟨i✝, hi⟩ = ⟨i.succ, hi✝⟩
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i✝, hi⟩
Tactic:
cases heq
State after:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩

State before:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
rw [Nat.add_comm] at h
State after:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩

State before:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
have : (encodeFun fun k => x (succ k)) = k / n := by
  rw [←h]
  rw [Nat.add_mul_div_left (H := hnpos)]
  rw [Nat.div_eq_of_lt (x 0).isLt]
  rw [Nat.zero_add]
State after:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩

State before:
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
transitivity ((decodeFun (encodeFun fun k => x (succ k))) ⟨i, Nat.lt_of_succ_lt_succ hi⟩)
State after:
case refl.left
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = (encodeFun fun k => x k.succ).decodeFun ⟨i, ⋯⟩

case refl.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (encodeFun fun k => x k.succ).decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ↑(encodeFun fun k => x k.succ) = k / n
Tactic:
rw [←h]
State after:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ↑(encodeFun fun k => x k.succ) = (↑(x 0) + n * ↑(encodeFun fun k => x k.succ)) / n

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ↑(encodeFun fun k => x k.succ) = (↑(x 0) + n * ↑(encodeFun fun k => x k.succ)) / n
Tactic:
rw [Nat.add_mul_div_left (H := hnpos)]
State after:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ↑(encodeFun fun k => x k.succ) = ↑(x 0) / n + ↑(encodeFun fun k => x k.succ)

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ↑(encodeFun fun k => x k.succ) = ↑(x 0) / n + ↑(encodeFun fun k => x k.succ)
Tactic:
rw [Nat.div_eq_of_lt (x 0).isLt]
State after:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ↑(encodeFun fun k => x k.succ) = 0 + ↑(encodeFun fun k => x k.succ)

State before:
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ↑(encodeFun fun k => x k.succ) = 0 + ↑(encodeFun fun k => x k.succ)
Tactic:
rw [Nat.zero_add]
State after:
no goals

State before:
case refl.left
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = (encodeFun fun k => x k.succ).decodeFun ⟨i, ⋯⟩
Tactic:
congr
State after:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ k / n = ↑(encodeFun fun k => x k.succ)

State before:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ k / n = ↑(encodeFun fun k => x k.succ)
Tactic:
rw [←h]
State after:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (↑(x 0) + n * ↑(encodeFun fun k => x k.succ)) / n = ↑(encodeFun fun k => x k.succ)

State before:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (↑(x 0) + n * ↑(encodeFun fun k => x k.succ)) / n = ↑(encodeFun fun k => x k.succ)
Tactic:
rw [Nat.add_mul_div_left (H := hnpos)]
State after:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ ↑(x 0) / n + ↑(encodeFun fun k => x k.succ) = ↑(encodeFun fun k => x k.succ)

State before:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ ↑(x 0) / n + ↑(encodeFun fun k => x k.succ) = ↑(encodeFun fun k => x k.succ)
Tactic:
rw [Nat.div_eq_of_lt (x 0).isLt]
State after:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ 0 + ↑(encodeFun fun k => x k.succ) = ↑(encodeFun fun k => x k.succ)

State before:
case refl.left.e_a.e_val
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ 0 + ↑(encodeFun fun k => x k.succ) = ↑(encodeFun fun k => x k.succ)
Tactic:
rw [Nat.zero_add]
State after:
no goals

State before:
case refl.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (encodeFun fun k => x k.succ).decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
rw [ih1]
State after:
case refl.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (fun k => x k.succ) ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩

State before:
case refl.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (fun k => x k.succ) ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
rfl
State after:
no goals