internlm/Lean-Github huggingface dataset:
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)
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, ⋯⟩
Tactic:
assumption
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
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:
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ encodeSubtype p ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = 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
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ encodeSubtype p ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = k
Tactic:
simp only [encodeSubtype, dif_pos h0]
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1, ⋯⟩ = 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
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1, ⋯⟩ = 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
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ↑(⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1, ⋯⟩) = ↑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
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ↑(⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1, ⋯⟩) = ↑k
Tactic:
simp only [val_ndrec]
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
heq : ↑k = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1 = ↑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)
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
isLt✝ : 0 < count p
heq : ↑⟨0, isLt✝⟩ = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1 = ↑⟨0, isLt✝⟩
Tactic:
contradiction
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)
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
k : Nat
hk : k + 1 < count p
heq : ↑⟨k + 1, hk⟩ = k✝.succ
heq✝ : ⋯ ≅ hk✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1 = ↑⟨k + 1, hk⟩
Tactic:
injection heq with hkk
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1 = ↑⟨k + 1, hk⟩
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)
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
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) + 1 = ↑⟨k + 1, hk⟩
Tactic:
congr 1
Proof state after:
case e_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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) = k
Theorem: Fin.specSubtype
Proof state before:
case e_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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) = k
Tactic:
transitivity (Fin.mk k (Nat.lt_of_succ_lt_succ (this ▸ hk))).val
Proof state after:
case e_a.left
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) = ↑⟨k, ⋯⟩

case e_a.right
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑⟨k, ⋯⟩ = k
Theorem: Fin.specSubtype
Proof state before:
case e_a.left
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩) = ↑⟨k, ⋯⟩
Tactic:
apply Fin.val_eq_of_eq
Proof state after:
case e_a.left.h
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩ = ⟨k, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_a.left.h
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩, ⋯⟩ = ⟨k, ⋯⟩
Tactic:
simp only [Nat.add_eq, Nat.add_zero, Fin.eta]
Proof state after:
case e_a.left.h
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ encodeSubtype (fun i => p i.succ) ⟨(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩ = ⟨k, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_a.left.h
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ encodeSubtype (fun i => p i.succ) ⟨(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩ = ⟨k, ⋯⟩
Tactic:
rw [←ih]
Proof state after:
case e_a.left.h
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩ = ⟨(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_a.left.h
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩ = ⟨(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1, ⋯⟩
Tactic:
congr
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
case e_a.right
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
k✝ : Nat
hk✝ : k✝ + 1 < count p
k : Nat
hk : k + 1 < count p
heq✝ : ⋯ ≅ hk✝
hkk : k = k✝
⊢ ↑⟨k, ⋯⟩ = k
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
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
⊢ encodeSubtype p i = k
Tactic:
have : count p = count (fun i => p (succ i)) := by
  simp_arith only [count, sum_succ, if_neg 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 : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
this : count p = count fun i => p i.succ
⊢ 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 : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
⊢ count p = count fun i => p i.succ
Tactic:
simp_arith only [count, sum_succ, if_neg 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 : ⟨⟨↑(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 : ⟨⟨↑(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
val✝ : Nat
isLt✝¹ : val✝ < count p
isLt✝ : 0 < n + 1
property✝ : p ⟨0, isLt✝⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨val✝, isLt✝¹⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨0, isLt✝⟩, property✝⟩
⊢ encodeSubtype p ⟨⟨0, isLt✝⟩, property✝⟩ = ⟨val✝, isLt✝¹⟩
Tactic:
contradiction
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
Tactic:
apply Fin.eq
Proof state after:
case 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)
i✝ : { i // p i }
h0 : ¬p 0
this : count p = count fun i => p i.succ
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k, hk⟩
Theorem: Fin.specSubtype
Proof state before:
case 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)
i✝ : { i // p i }
h0 : ¬p 0
this : count p = count fun i => p i.succ
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k, hk⟩
Tactic:
simp only [encodeSubtype, dif_neg h0, val_ndrec]
Proof state after:
case 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)
i✝ : { i // p i }
h0 : ¬p 0
this : count p = count fun i => p i.succ
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
Theorem: Fin.specSubtype
Proof state before:
case 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)
i✝ : { i // p i }
h0 : ¬p 0
this : count p = count fun i => p i.succ
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
Tactic:
clean at h
Proof state after:
case 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)
i✝ : { i // p i }
h0 : ¬p 0
this : count p = count fun i => p i.succ
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
Theorem: Fin.specSubtype
Proof state before:
case 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)
i✝ : { i // p i }
h0 : ¬p 0
this : count p = count fun i => p i.succ
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
Tactic:
transitivity (Fin.mk k (this ▸ hk)).val
Proof state after:
case a.left
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩

case a.right
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑⟨k, ⋯⟩ = k
Theorem: Fin.specSubtype
Proof state before:
case a.left
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Tactic:
apply Fin.val_eq_of_eq
Proof state after:
case a.left.h
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case a.left.h
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k, ⋯⟩
Tactic:
rw [←ih]
Proof state after:
case a.left.h
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩