internlm/Lean-Github huggingface dataset:
Theorem: Fin.specPi
Proof 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
Proof 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'⟩
Theorem: Fin.specPi
Proof 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
Proof 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
Theorem: Fin.specPi
Proof 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]
Proof 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
Theorem: Fin.specPi
Proof 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]
Proof 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, ⋯⟩)
Theorem: Fin.specPi
Proof 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]
Proof 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, ⋯⟩)
Theorem: Fin.specPi
Proof 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]
Proof 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, ⋯⟩)
Theorem: Fin.specPi
Proof 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
Proof state after:
no goals
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)
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
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)
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]
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)
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⟩)
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)
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
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
case zero
p : Fin 0 → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
⊢ decodeSubtype p k = i ↔ encodeSubtype p i = k
Tactic:
simp [count, sum] at k
Proof state after:
case zero
p : Fin 0 → Prop
inst : DecidablePred p
k : Fin 0
i : { i // p i }
⊢ decodeSubtype p k = i ↔ encodeSubtype p i = k
Theorem: Fin.specSubtype
Proof state before:
case zero
p : Fin 0 → Prop
inst : DecidablePred p
k : Fin 0
i : { i // p i }
⊢ decodeSubtype p k = i ↔ encodeSubtype p i = k
Tactic:
cases k
Proof state after:
case zero.mk
p : Fin 0 → Prop
inst : DecidablePred p
i : { i // p i }
val✝ : Nat
isLt✝ : val✝ < 0
⊢ decodeSubtype p ⟨val✝, isLt✝⟩ = i ↔ encodeSubtype p i = ⟨val✝, isLt✝⟩
Theorem: Fin.specSubtype
Proof state before:
case zero.mk
p : Fin 0 → Prop
inst : DecidablePred p
i : { i // p i }
val✝ : Nat
isLt✝ : val✝ < 0
⊢ decodeSubtype p ⟨val✝, isLt✝⟩ = i ↔ encodeSubtype p i = ⟨val✝, isLt✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
case succ
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
⊢ decodeSubtype p k = i ↔ encodeSubtype p i = k
Tactic:
constructor
Proof state after:
case succ.mp
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
⊢ decodeSubtype p k = i → encodeSubtype p i = k

case succ.mpr
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
⊢ encodeSubtype p i = k → decodeSubtype p k = i
Theorem: Fin.specSubtype
Proof state before:
case succ.mp
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
⊢ decodeSubtype p k = i → encodeSubtype p i = k
Tactic:
intro h
Proof state after:
case succ.mp
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h : decodeSubtype p k = i
⊢ encodeSubtype p i = k
Theorem: Fin.specSubtype
Proof state before:
case succ.mp
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h : decodeSubtype p k = i
⊢ encodeSubtype p i = k
Tactic:
simp only [decodeSubtype] at h
Proof state after:
case succ.mp
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h :
  (if h : p 0 then
      match ↑k, ⋯ with
      | 0, hk => ⟨0, ⋯⟩
      | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩
    else ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ encodeSubtype p i = k
Theorem: Fin.specSubtype
Proof state before:
case succ.mp
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h :
  (if h : p 0 then
      match ↑k, ⋯ with
      | 0, hk => ⟨0, ⋯⟩
      | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩
    else ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ encodeSubtype p i = k
Tactic:
split at h
Proof state after:
case succ.mp.isTrue
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h✝ : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ encodeSubtype p i = k

case succ.mp.isFalse
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h✝ : ¬p 0
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
⊢ encodeSubtype p i = k
Theorem: Fin.specSubtype
Proof state before:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ encodeSubtype p i = k
Tactic:
have : count p = count (fun i => p (succ i)) + 1 := by
  simp_arith only [count, sum_succ, if_pos h0]; rfl
Proof state after:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
this : count p = (count fun i => p i.succ) + 1
⊢ encodeSubtype p i = k
Theorem: Fin.specSubtype
Proof state before:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
this : count p = (count fun i => p i.succ) + 1
⊢ encodeSubtype p i = k
Tactic:
split at h
Proof state after:
case h_1
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
h : ⟨0, ⋯⟩ = i
⊢ encodeSubtype p i = k

case h_2
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝¹ : Nat
hk✝¹ : k✝¹ < count p
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq✝¹ : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
⊢ encodeSubtype p i = k
Theorem: Fin.specSubtype
Proof state before:
case h_1
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
h : ⟨0, ⋯⟩ = i
⊢ encodeSubtype p i = k

case h_2
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝¹ : Nat
hk✝¹ : k✝¹ < count p
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq✝¹ : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
⊢ encodeSubtype p i = k
Tactic:
next =>
  cases h
  simp only [encodeSubtype]
  apply Fin.eq
  symmetry
  assumption
Proof state after:
case h_2
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝¹ : Nat
hk✝¹ : k✝¹ < count p
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq✝¹ : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
⊢ encodeSubtype p i = k
Theorem: Fin.specSubtype
Proof state before:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ count p = (count fun i => p i.succ) + 1
Tactic:
simp_arith only [count, sum_succ, if_pos h0]
Proof state after:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ sum ((fun i => if p i then 1 else 0) ∘ succ) = sum fun i => if p i.succ then 1 else 0
Theorem: Fin.specSubtype
Proof state before:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
h :
  (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
⊢ sum ((fun i => if p i then 1 else 0) ∘ succ) = sum fun i => if p i.succ then 1 else 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
h : ⟨0, ⋯⟩ = i
⊢ encodeSubtype p i = k
Tactic:
cases h
Proof state after:
case refl
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ encodeSubtype p ⟨0, ⋯⟩ = k
Theorem: Fin.specSubtype
Proof state before:
case refl
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ encodeSubtype p ⟨0, ⋯⟩ = k
Tactic:
simp only [encodeSubtype]
Proof state after:
case refl
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ ⟨0, ⋯⟩ = k
Theorem: Fin.specSubtype
Proof state before:
case refl
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ ⟨0, ⋯⟩ = k
Tactic:
apply Fin.eq
Proof state after:
case refl.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ ↑⟨0, ⋯⟩ = ↑k
Theorem: Fin.specSubtype
Proof state before:
case refl.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ ↑⟨0, ⋯⟩ = ↑k
Tactic:
symmetry
Proof state after:
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
heq✝¹ : ↑k = 0
heq✝ : ⋯ ≅ hk✝
⊢ ↑k = ↑⟨0, ⋯⟩