rw [Nat.add_mul_mod_self_left]
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✝⟩)
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✝⟩)