internlm/Lean-Github huggingface dataset:
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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
Proof 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⟩
Theorem: Fin.specFun
Proof 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
Proof 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⟩
Theorem: Fin.specFun
Proof 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
Proof 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⟩
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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)
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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]
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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]
Proof 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
Theorem: Fin.specFun
Proof 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
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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]
Proof 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
Theorem: Fin.specFun
Proof 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
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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]
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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]
Proof 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
Theorem: Fin.specFun
Proof 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 ..
Proof state after:
no goals
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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
Theorem: Fin.specFun
Proof 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
Proof 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