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