internlm/Lean-Github huggingface dataset:
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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
congr
Proof state after:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 = i
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 = i
Tactic:
transitivity (⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ : { i // p (succ i) }).val.val
Proof state after:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 = ↑⟨⟨i, ⋯⟩, hp⟩.val

case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ ↑⟨⟨i, ⋯⟩, hp⟩.val = i
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
⊢ decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
Tactic:
rw [ih]
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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Tactic:
simp only [encodeSubtype, dif_pos h0] at h
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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
heq✝ : ⋯ ≅ hk'
h : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨k'.succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
heq✝ : ⋯ ≅ hk'
h : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨k'.succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Tactic:
let h := val_eq_of_eq h
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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
heq✝ : ⋯ ≅ hk'
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨k'.succ, hk⟩
h : ↑(⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩) = ↑⟨k'.succ, hk⟩ := val_eq_of_eq h✝
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
heq✝ : ⋯ ≅ hk'
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨k'.succ, hk⟩
h : ↑(⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩) = ↑⟨k'.succ, hk⟩ := val_eq_of_eq h✝
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Tactic:
rw [val_ndrec] at h
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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
heq✝ : ⋯ ≅ hk'
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨k'.succ, hk⟩
h : ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ↑⟨k'.succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
heq✝ : ⋯ ≅ hk'
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨k'.succ, hk⟩
h : ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ↑⟨k'.succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨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)
i✝ : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk' : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1 < count p
hk : (↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ < count p
heq✝ : ⋯ ≅ hk'
h :
  ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ =
    ⟨(↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩
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)
i✝ : { i // p i }
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk' : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1 < count p
hk : (↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ < count p
heq✝ : ⋯ ≅ hk'
h :
  ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ =
    ⟨(↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 = ↑⟨⟨i, ⋯⟩, hp⟩.val
Tactic:
apply congrArg Fin.val
Proof state after:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ (decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 = ⟨⟨i, ⋯⟩, hp⟩.val
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ (decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 = ⟨⟨i, ⋯⟩, hp⟩.val
Tactic:
apply congrArg Subtype.val
Proof state after:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
Tactic:
simp only [Nat.add_eq, Nat.add_zero, ih]
Proof state after:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Tactic:
have h := Fin.val_eq_of_eq h
Proof state after:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
h : ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k'.succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
h : ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k'.succ, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Tactic:
simp only [encodeSubtype, dif_pos h0, val_ndrec] at h
Proof state after:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
h : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1 = k'.succ
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
h : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1 = k'.succ
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k', ⋯⟩
Tactic:
cases h
Proof state after:
case refl.e_val.e_val.e_a.left.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)
i✝ : { i // p i }
h0 : p 0
this✝ : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk' : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1 < count p
hk : (↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨(↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.e_a.left.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)
i✝ : { i // p i }
h0 : p 0
this✝ : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk' : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1 < count p
hk : (↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨(↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩)).succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
case refl.e_val.e_val.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)
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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : k'.succ < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k'.succ, hk⟩
heq✝ : ⋯ ≅ hk'
this : decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
⊢ ↑⟨⟨i, ⋯⟩, hp⟩.val = i
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
k : Nat
hk : k < count p
isLt✝ : 0 < n + 1
hp : p ⟨0, isLt✝⟩
h : encodeSubtype p ⟨⟨0, isLt✝⟩, hp⟩ = ⟨k, hk⟩
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨0, isLt✝⟩, hp⟩
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
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
congr
Proof state after:
case e_val.e_val.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)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = i
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.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)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = i
Tactic:
transitivity (⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ : { i // p (succ i) }).val.val
Proof state after:
case e_val.e_val.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)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = ↑⟨⟨i, ⋯⟩, hp⟩.val

case e_val.e_val.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)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑⟨⟨i, ⋯⟩, hp⟩.val = i