internlm/Lean-Github huggingface dataset:
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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
Proof 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⟩
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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 ⟨_,_⟩
Proof 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✝⟩
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ encodePi f x = ⟨k, hk⟩
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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(encodePi f x) = ↑⟨k, hk⟩
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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ ↑(encodePi f x) = ↑⟨k, hk⟩
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)
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
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)
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)
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)
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
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ 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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ 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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
⊢ 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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
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)
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
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)
k : Nat
hk✝ : k < prod f
hk : k < 0
h : decodePi f ⟨k, hk✝⟩ = x
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)
k : Nat
hk✝ : k < prod f
hk : k < 0
h : decodePi f ⟨k, hk✝⟩ = x
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)
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]
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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
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)
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]
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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
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)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
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)
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]
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)
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
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)
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
Proof 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
Theorem: Fin.specPi
Proof 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]
Proof 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
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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]
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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]
Proof 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
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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]
Proof 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
Theorem: Fin.specPi
Proof 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 ..
Proof state after:
no goals
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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
Proof 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
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)
⊢ decodePi f k i = x i
Tactic:
simp only [decodePi]
Proof 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