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

State before:
case zero
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
⊢ decodePi f k = x ↔ encodePi f x = k
Tactic:
constructor
State after:
case zero.mp
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
⊢ decodePi f k = x → encodePi f x = k

case zero.mpr
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
⊢ encodePi f x = k → decodePi f k = x

State before:
case zero.mp
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
⊢ decodePi f k = x → encodePi f x = k
Tactic:
intro
State after:
case zero.mp
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
a✝ : decodePi f k = x
⊢ encodePi f x = k

State before:
case zero.mp
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
a✝ : decodePi f k = x
⊢ encodePi f x = k
Tactic:
match k with
| ⟨0, _⟩ => rfl
| ⟨_+1, h⟩ => simp [prod] at h; contradiction
State after:
no goals

State before:
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
isLt✝ : 0 < prod f
a✝ : decodePi f ⟨0, isLt✝⟩ = x
⊢ encodePi f x = ⟨0, isLt✝⟩
Tactic:
rfl
State after:
no goals

State before:
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
n✝ : Nat
h : n✝ + 1 < prod f
a✝ : decodePi f ⟨n✝ + 1, h⟩ = x
⊢ encodePi f x = ⟨n✝ + 1, h⟩
Tactic:
simp [prod] at h
State after:
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
n✝ : Nat
h : n✝ + 1 < 1
a✝ : decodePi f ⟨n✝ + 1, h⟩ = x
⊢ encodePi f x = ⟨n✝ + 1, h⟩

State before:
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
n✝ : Nat
h : n✝ + 1 < 1
a✝ : decodePi f ⟨n✝ + 1, h⟩ = x
⊢ encodePi f x = ⟨n✝ + 1, h⟩
Tactic:
contradiction
State after:
no goals

State before:
case zero.mpr
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
⊢ encodePi f x = k → decodePi f k = x
Tactic:
intro
State after:
case zero.mpr
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
a✝ : encodePi f x = k
⊢ decodePi f k = x

State before:
case zero.mpr
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
a✝ : encodePi f x = k
⊢ decodePi f k = x
Tactic:
funext ⟨_,_⟩
State after:
case zero.mpr.h
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
a✝ : encodePi f x = k
val✝ : Nat
isLt✝ : val✝ < 0
⊢ decodePi f k ⟨val✝, isLt✝⟩ = x ⟨val✝, isLt✝⟩

State before:
case zero.mpr.h
f : Fin 0 → Nat
k : Fin (prod f)
x : (i : Fin 0) → Fin (f i)
a✝ : encodePi f x = k
val✝ : Nat
isLt✝ : val✝ < 0
⊢ decodePi f k ⟨val✝, isLt✝⟩ = x ⟨val✝, isLt✝⟩
Tactic:
contradiction
State after:
no goals

State before:
case succ
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
⊢ decodePi f k = x ↔ encodePi f x = k
Tactic:
constructor
State after:
case succ.mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
⊢ decodePi f k = x → encodePi f x = k

case succ.mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
⊢ encodePi f x = k → decodePi f k = x

State before:
case succ.mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
⊢ decodePi f k = x → encodePi f x = k
Tactic:
intro h
State after:
case succ.mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : decodePi f k = x
⊢ encodePi f x = k

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ encodePi f x = ⟨k, hk⟩
Tactic:
apply Fin.eq
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(encodePi f x) = ↑⟨k, hk⟩

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(encodePi f x) = ↑⟨k, hk⟩
Tactic:
simp only [encodePi]
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) = k

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) = k
Tactic:
transitivity (f 0 * (k / f 0) + k % f 0)
State after:
case a.left
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) = f 0 * (k / f 0) + k % f 0

case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * (k / f 0) + k % f 0 = k

State before:
case a.left
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) = f 0 * (k / f 0) + k % f 0
Tactic:
congr 1
State after:
case a.left.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = f 0 * (k / f 0)

case a.left.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(x 0) = k % f 0

State before:
case a.left.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = f 0 * (k / f 0)
Tactic:
congr 1
State after:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0

State before:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0
Tactic:
have hpos : f 0 > 0 := by
  apply Nat.pos_of_nonzero
  intro hz
  rw [prod_succ, hz, Nat.zero_mul] at hk
  contradiction
State after:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0

State before:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0
Tactic:
have hk' : k / f 0 < Fin.prod (f ∘ succ) := by
  rw [Nat.div_lt_iff_lt_mul hpos]
  rw [Nat.mul_comm, ←prod_succ]
  exact hk
State after:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0

State before:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0
Tactic:
have : encodePi (fun i => f (succ i)) (fun i => x (succ i)) = ⟨k / f 0, hk'⟩ := by
  rw [←ih]
  funext i
  rw [←h]
  rfl
State after:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0

State before:
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0
Tactic:
transitivity (encodePi (fun i => f (succ i)) (fun i => x (succ i))).val
State after:
case a.left.e_a.e_a.left
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = ↑(encodePi (fun i => f i.succ) fun i => x i.succ)

case a.left.e_a.e_a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = k / f 0

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 > 0
Tactic:
apply Nat.pos_of_nonzero
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 ≠ 0

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 ≠ 0
Tactic:
intro hz
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hz : f 0 = 0
⊢ False

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hz : f 0 = 0
⊢ False
Tactic:
rw [prod_succ, hz, Nat.zero_mul] at hk
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk✝ : k < prod f
hk : k < 0
h : decodePi f ⟨k, hk✝⟩ = x
hz : f 0 = 0
⊢ False

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk✝ : k < prod f
hk : k < 0
h : decodePi f ⟨k, hk✝⟩ = x
hz : f 0 = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ k / f 0 < prod (f ∘ succ)
Tactic:
rw [Nat.div_lt_iff_lt_mul hpos]
State after:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ k < prod (f ∘ succ) * f 0

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ k < prod (f ∘ succ) * f 0
Tactic:
rw [Nat.mul_comm, ←prod_succ]
State after:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ k < prod f

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ k < prod f
Tactic:
exact hk
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
Tactic:
rw [←ih]
State after:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
Tactic:
funext i
State after:
case h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
i : Fin n
⊢ decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ i = x i.succ

State before:
case h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
i : Fin n
⊢ decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ i = x i.succ
Tactic:
rw [←h]
State after:
case h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
i : Fin n
⊢ decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ i = decodePi f ⟨k, hk⟩ i.succ

State before:
case h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
i : Fin n
⊢ decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ i = decodePi f ⟨k, hk⟩ i.succ
Tactic:
rfl
State after:
no goals

State before:
case a.left.e_a.e_a.left
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = ↑(encodePi (fun i => f i.succ) fun i => x i.succ)
Tactic:
rfl
State after:
no goals

State before:
case a.left.e_a.e_a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = k / f 0
Tactic:
rw [this]
State after:
no goals

State before:
case a.left.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(x 0) = k % f 0
Tactic:
rw [←h]
State after:
case a.left.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(decodePi f ⟨k, hk⟩ 0) = k % f 0

State before:
case a.left.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(decodePi f ⟨k, hk⟩ 0) = k % f 0
Tactic:
rfl
State after:
no goals

State before:
case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ f 0 * (k / f 0) + k % f 0 = k
Tactic:
rw [Nat.add_comm]
State after:
case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ k % f 0 + f 0 * (k / f 0) = k

State before:
case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ k % f 0 + f 0 * (k / f 0) = k
Tactic:
exact Nat.mod_add_div ..
State after:
no goals

State before:
case succ.mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
⊢ encodePi f x = k → decodePi f k = x
Tactic:
intro h
State after:
case succ.mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
⊢ decodePi f k = x

State before:
case succ.mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
⊢ decodePi f k = x
Tactic:
funext i
State after:
case succ.mpr.h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
i : Fin (n + 1)
⊢ decodePi f k i = x i

State before:
case succ.mpr.h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
i : Fin (n + 1)
⊢ decodePi f k i = x i
Tactic:
simp only [decodePi]
State after:
case succ.mpr.h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
i : Fin (n + 1)
⊢ (match i with
    | ⟨0, isLt⟩ => ⟨↑k % f 0, ⋯⟩
    | ⟨i.succ, hi⟩ => decodePi (f ∘ succ) ⟨↑k / f 0, ⋯⟩ ⟨i, ⋯⟩) =
    x i

State before:
case succ.mpr.h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
i : Fin (n + 1)
⊢ (match i with
    | ⟨0, isLt⟩ => ⟨↑k % f 0, ⋯⟩
    | ⟨i.succ, hi⟩ => decodePi (f ∘ succ) ⟨↑k / f 0, ⋯⟩ ⟨i, ⋯⟩) =
    x i
Tactic:
split
State after:
case succ.mpr.h.h_1
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ⟨↑k % f 0, ⋯⟩ = x ⟨0, isLt✝⟩

case succ.mpr.h.h_2
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
i✝ : Nat
hi✝ : i✝ + 1 < n + 1
⊢ decodePi (f ∘ succ) ⟨↑k / f 0, ⋯⟩ ⟨i✝, ⋯⟩ = x ⟨i✝.succ, hi✝⟩

State before:
case succ.mpr.h.h_1
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ⟨↑k % f 0, ⋯⟩ = x ⟨0, isLt✝⟩

case succ.mpr.h.h_2
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
i✝ : Nat
hi✝ : i✝ + 1 < n + 1
⊢ decodePi (f ∘ succ) ⟨↑k / f 0, ⋯⟩ ⟨i✝, ⋯⟩ = x ⟨i✝.succ, hi✝⟩
Tactic:
next =>
  apply Fin.eq
  clean
  rw [←h]
  simp only [encodePi]
  rw [Nat.add_comm]
  rw [Nat.add_mul_mod_self_left]
  rw [Nat.mod_eq_of_lt]
  rfl
  exact (x 0).isLt
State after:
case succ.mpr.h.h_2
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
i✝ : Nat
hi✝ : i✝ + 1 < n + 1
⊢ decodePi (f ∘ succ) ⟨↑k / f 0, ⋯⟩ ⟨i✝, ⋯⟩ = x ⟨i✝.succ, hi✝⟩

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ⟨↑k % f 0, ⋯⟩ = x ⟨0, isLt✝⟩
Tactic:
apply Fin.eq
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑⟨↑k % f 0, ⋯⟩ = ↑(x ⟨0, isLt✝⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑⟨↑k % f 0, ⋯⟩ = ↑(x ⟨0, isLt✝⟩)
Tactic:
clean
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑k % f 0 = ↑(x ⟨0, isLt✝⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑k % f 0 = ↑(x ⟨0, isLt✝⟩)
Tactic:
rw [←h]
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(encodePi f x) % f 0 = ↑(x ⟨0, isLt✝⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(encodePi f x) % f 0 = ↑(x ⟨0, isLt✝⟩)
Tactic:
simp only [encodePi]
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) % f 0 = ↑(x ⟨0, isLt✝⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) % f 0 = ↑(x ⟨0, isLt✝⟩)
Tactic:
rw [Nat.add_comm]
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ (↑(x 0) + f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)) % f 0 = ↑(x ⟨0, isLt✝⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ (↑(x 0) + f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)) % f 0 = ↑(x ⟨0, isLt✝⟩)
Tactic:
rw [Nat.add_mul_mod_self_left]
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) % f 0 = ↑(x ⟨0, isLt✝⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) % f 0 = ↑(x ⟨0, isLt✝⟩)
Tactic:
rw [Nat.mod_eq_of_lt]
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) = ↑(x ⟨0, isLt✝⟩)

case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) < f 0

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) = ↑(x ⟨0, isLt✝⟩)

case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) < f 0
Tactic:
rfl
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) < f 0

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ↑(x 0) < f 0
Tactic:
exact (x 0).isLt
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : encodePi f x = ⟨k, hk⟩
⊢ decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
simp only [encodePi] at h
State after:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
apply Fin.eq
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)
Tactic:
have hpos : f 0 > 0 := by
  apply Nat.pos_of_nonzero
  intro hz
  rw [prod_succ, hz, Nat.zero_mul] at hk
  contradiction
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)
Tactic:
have hk' : k / f 0 < Fin.prod (f ∘ succ) := by
  rw [Nat.div_lt_iff_lt_mul hpos]
  rw [Nat.mul_comm, ←prod_succ]
  exact hk
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)
Tactic:
have : decodePi (fun i => f (succ i)) ⟨k / f 0, hk'⟩ = fun i => x (succ i) := by
  rw [ih]
  cases h
  apply Fin.eq
  clean
  rw [Nat.add_comm]
  rw [Nat.add_mul_div_left _ _ hpos]
  rw [Nat.div_eq_of_lt (x 0).isLt]
  rw [Nat.zero_add]
  rfl
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)
Tactic:
clean
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (f ∘ succ) ⟨k / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (f ∘ succ) ⟨k / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)
Tactic:
transitivity (decodePi (fun i => f (succ i)) ⟨k / f 0, hk'⟩ ⟨i, Nat.lt_of_succ_lt_succ hi⟩).val
State after:
case a.left
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (f ∘ succ) ⟨k / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ ⟨i, ⋯⟩)

case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ f 0 > 0
Tactic:
apply Nat.pos_of_nonzero
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ f 0 ≠ 0

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ f 0 ≠ 0
Tactic:
intro hz
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hz : f 0 = 0
⊢ False

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hz : f 0 = 0
⊢ False
Tactic:
rw [prod_succ, hz, Nat.zero_mul] at hk
State after:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk✝ : k < prod f
hk : k < 0
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk✝⟩
hz : f 0 = 0
⊢ False

State before:
case a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk✝ : k < prod f
hk : k < 0
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk✝⟩
hz : f 0 = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
⊢ k / f 0 < prod (f ∘ succ)
Tactic:
rw [Nat.div_lt_iff_lt_mul hpos]
State after:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
⊢ k < prod (f ∘ succ) * f 0

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
⊢ k < prod (f ∘ succ) * f 0
Tactic:
rw [Nat.mul_comm, ←prod_succ]
State after:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
⊢ k < prod f

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
⊢ k < prod f
Tactic:
exact hk
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
Tactic:
rw [ih]
State after:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩

State before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ (encodePi (fun i => f i.succ) fun i => x i.succ) = ⟨k / f 0, hk'⟩
Tactic:
cases h
State after:
case refl
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ (encodePi (fun i => f i.succ) fun i => x i.succ) =
    ⟨(f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0, hk'⟩

State before:
case refl
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ (encodePi (fun i => f i.succ) fun i => x i.succ) =
    ⟨(f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0, hk'⟩
Tactic:
apply Fin.eq
State after:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) =
    ↑⟨(f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0, hk'⟩

State before:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) =
    ↑⟨(f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0, hk'⟩
Tactic:
clean
State after:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) =
    (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0

State before:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) =
    (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0
Tactic:
rw [Nat.add_comm]
State after:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) =
    (↑(x 0) + f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)) / f 0

State before:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) =
    (↑(x 0) + f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)) / f 0
Tactic:
rw [Nat.add_mul_div_left _ _ hpos]
State after:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = ↑(x 0) / f 0 + ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)

State before:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = ↑(x 0) / f 0 + ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)
Tactic:
rw [Nat.div_eq_of_lt (x 0).isLt]
State after:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = 0 + ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)

State before:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = 0 + ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)
Tactic:
rw [Nat.zero_add]
State after:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)

State before:
case refl.a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)
Tactic:
rfl
State after:
no goals

State before:
case a.left
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (f ∘ succ) ⟨k / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ ⟨i, ⋯⟩)
Tactic:
rfl
State after:
no goals

State before:
case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑(decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)
Tactic:
rw [this]
State after:
case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑((fun i => x i.succ) ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)

State before:
case a.right
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
this : decodePi (fun i => f i.succ) ⟨k / f 0, hk'⟩ = fun i => x i.succ
⊢ ↑((fun i => x i.succ) ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)
Tactic:
rfl
State after:
no goals