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