internlm/Lean-Github huggingface dataset:
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⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
Tactic:
cases h
Proof state after:
case a.left.h.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
k : Nat
hk : k < count p
hi : ↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1 < n + 1
hp : p ⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, hi⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩ = ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1, ⋯⟩, hp⟩
Theorem: Fin.specSubtype
Proof state before:
case a.left.h.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
k : Nat
hk : k < count p
hi : ↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1 < n + 1
hp : p ⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, hi⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩ = ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1, ⋯⟩, hp⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
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
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
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
Tactic:
intro h
Proof state after:
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 }
h : encodeSubtype p i = k
⊢ decodeSubtype p k = i
Theorem: Fin.specSubtype
Proof state before:
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 }
h : encodeSubtype p i = k
⊢ decodeSubtype p k = i
Tactic:
simp only [decodeSubtype]
Proof state after:
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 }
h : encodeSubtype p i = k
⊢ (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
Theorem: Fin.specSubtype
Proof state before:
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 }
h : encodeSubtype p i = k
⊢ (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
Tactic:
split
Proof state after:
case succ.mpr.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 : encodeSubtype p i = k
h✝ : p 0
⊢ (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i

case succ.mpr.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 : encodeSubtype p i = k
h✝ : ¬p 0
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨↑k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = 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 }
h : encodeSubtype p i = k
h0 : p 0
⊢ (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
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 }
h : encodeSubtype p i = k
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
⊢ (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    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 }
h : encodeSubtype p i = k
h0 : p 0
this : count p = (count fun i => p i.succ) + 1
⊢ (match ↑k, ⋯ with
    | 0, hk => ⟨0, ⋯⟩
    | k.succ, hk => ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩) =
    i
Tactic:
split
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 }
h : encodeSubtype p i = k
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, ⋯⟩ = i

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 }
h : encodeSubtype p i = k
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✝
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
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 }
h : encodeSubtype p i = k
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, ⋯⟩ = i

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 }
h : encodeSubtype p i = k
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✝
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = i
Tactic:
next heq _ =>
  match k, i with
  | ⟨_,_⟩, ⟨⟨0,_⟩, _⟩ => rfl
  | ⟨k,hk⟩, ⟨⟨i+1,hi⟩, hp⟩ =>
    cases heq
    simp only [encodeSubtype, dif_pos h0] at h
    have h := val_eq_of_eq h
    rw [val_ndrec] at h
    contradiction
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 }
h : encodeSubtype p i = k
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✝
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k✝, ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = 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 }
h : encodeSubtype p i = k
h0 : p 0
⊢ 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 }
h : encodeSubtype p i = k
h0 : p 0
⊢ 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 }
h : encodeSubtype p i = k
h0 : p 0
⊢ 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 }
h : encodeSubtype p i = k
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, ⋯⟩ = i
Tactic:
match k, i with
| ⟨_,_⟩, ⟨⟨0,_⟩, _⟩ => rfl
| ⟨k,hk⟩, ⟨⟨i+1,hi⟩, hp⟩ =>
  cases heq
  simp only [encodeSubtype, dif_pos h0] at h
  have h := val_eq_of_eq h
  rw [val_ndrec] at h
  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) + 1
k✝ : Nat
hk✝¹ : k✝ < count p
hk✝ : 0 < count p
val✝ : Nat
isLt✝¹ : val✝ < count p
isLt✝ : 0 < n + 1
property✝ : p ⟨0, isLt✝⟩
h : encodeSubtype p ⟨⟨0, isLt✝⟩, property✝⟩ = ⟨val✝, isLt✝¹⟩
heq : ↑⟨val✝, isLt✝¹⟩ = 0
heq✝ : ⋯ ≅ hk✝
⊢ ⟨0, ⋯⟩ = ⟨⟨0, isLt✝⟩, property✝⟩
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
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⟩
heq : ↑⟨k, hk⟩ = 0
heq✝ : ⋯ ≅ hk✝
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
cases heq
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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨0, hk⟩
heq✝ : ⋯ ≅ hk✝
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, 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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨0, hk⟩
heq✝ : ⋯ ≅ hk✝
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
simp only [encodeSubtype, dif_pos h0] at 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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, 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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
have h := val_eq_of_eq 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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
h : ↑(⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩) = ↑⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, 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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
h : ↑(⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩) = ↑⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
rw [val_ndrec] at 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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
h : ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ↑⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, 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
hk✝ : 0 < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : 0 < count p
heq✝ : ⋯ ≅ hk✝
h✝ : ⋯ ▸ ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ⟨0, hk⟩
h : ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) + 1, ⋯⟩ = ↑⟨0, hk⟩
⊢ ⟨0, ⋯⟩ = ⟨⟨i + 1, hi⟩, 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
this : count p = (count fun i => p i.succ) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
val✝ : Nat
isLt✝¹ : val✝ < count p
isLt✝ : 0 < n + 1
property✝ : p ⟨0, isLt✝⟩
h : encodeSubtype p ⟨⟨0, isLt✝⟩, property✝⟩ = ⟨val✝, isLt✝¹⟩
heq : ↑⟨val✝, isLt✝¹⟩ = k'.succ
heq✝ : ⋯ ≅ hk'
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨0, isLt✝⟩, property✝⟩
Tactic:
simp only [encodeSubtype] 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
val✝ : Nat
isLt✝¹ : val✝ < count p
isLt✝ : 0 < n + 1
property✝ : p ⟨0, isLt✝⟩
h : ⟨0, ⋯⟩ = ⟨val✝, isLt✝¹⟩
heq : ↑⟨val✝, isLt✝¹⟩ = k'.succ
heq✝ : ⋯ ≅ hk'
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨0, isLt✝⟩, property✝⟩
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
val✝ : Nat
isLt✝¹ : val✝ < count p
isLt✝ : 0 < n + 1
property✝ : p ⟨0, isLt✝⟩
h : ⟨0, ⋯⟩ = ⟨val✝, isLt✝¹⟩
heq : ↑⟨val✝, isLt✝¹⟩ = k'.succ
heq✝ : ⋯ ≅ hk'
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨0, isLt✝⟩, property✝⟩
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
k' : Nat
hk' : k' + 1 < count p
isLt✝¹ : 0 < n + 1
property✝ : p ⟨0, isLt✝¹⟩
isLt✝ : 0 < count p
heq : ↑⟨0, isLt✝⟩ = k'.succ
heq✝ : ⋯ ≅ hk'
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨0, isLt✝¹⟩, property✝⟩
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
isLt✝¹ : 0 < n + 1
property✝ : p ⟨0, isLt✝¹⟩
isLt✝ : 0 < count p
heq : ↑⟨0, isLt✝⟩ = k'.succ
heq✝ : ⋯ ≅ hk'
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨0, isLt✝¹⟩, property✝⟩
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) + 1
k✝ : Nat
hk✝ : k✝ < count p
k' : Nat
hk' : k' + 1 < count p
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⟩
heq : ↑⟨k, hk⟩ = k'.succ
heq✝ : ⋯ ≅ hk'
⊢ ⟨⟨↑(decodeSubtype (fun i => p i.succ) ⟨k', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
cases heq
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
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', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, 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
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', ⋯⟩).1 + 1, ⋯⟩, ⋯⟩ = ⟨⟨i + 1, hi⟩, hp⟩
Tactic:
have : decodeSubtype (fun i => p (succ i)) ⟨k', Nat.lt_of_add_lt_add_right (this ▸ hk')⟩ = ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ := by
  rw [ih]
  simp only [encodeSubtype, dif_pos h0] at h
  let h := val_eq_of_eq h
  rw [val_ndrec] at h
  cases h
  rfl
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
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⟩