Theorem: Fin.specSubtype (GMLInit/Data/Fin/Coding.lean)

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
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

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
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✝⟩

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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]
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

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
State after:
no goals

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
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

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]
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

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
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

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
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, ⋯⟩

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
State after:
no goals

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
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

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]
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

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
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

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]
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

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
State after:
no goals

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
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⟩

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
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

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
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

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
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, ⋯⟩

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]
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, ⋯⟩

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]
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, ⋯⟩

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
State after:
no goals

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
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⟩

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]
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

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
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

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
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

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
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, ⋯⟩

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]
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⟩

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
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⟩

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
State after:
no goals

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
State after:
no goals

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
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

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]
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

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
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

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
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

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
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

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
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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⟩

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
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⟩

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
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⟩

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
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⟩

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
State after:
no goals

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
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✝⟩

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
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✝⟩

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
State after:
no goals

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
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⟩

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
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⟩

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
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

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
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

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]
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', ⋯⟩

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
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', ⋯⟩

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
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', ⋯⟩

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
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', ⋯⟩

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
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⟩), ⋯⟩

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
State after:
no goals

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
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

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
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⟩

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]
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', ⋯⟩

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
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', ⋯⟩

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
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', ⋯⟩

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
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⟩), ⋯⟩

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

State before:
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
Tactic:
apply congrArg Fin.val
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

State before:
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
Tactic:
apply congrArg Subtype.val
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⟩, ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩

State before:
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⟩, ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
Tactic:
simp only [Nat.add_eq, Nat.add_zero, ih]
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⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k, ⋯⟩

State before:
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⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k, ⋯⟩
Tactic:
apply Fin.eq
State after:
case e_val.e_val.e_a.left.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⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩

State before:
case e_val.e_val.e_a.left.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⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Tactic:
have h := Fin.val_eq_of_eq h
State after:
case e_val.e_val.e_a.left.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⟩
h : ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k, hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩

State before:
case e_val.e_val.e_a.left.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⟩
h : ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k, hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Tactic:
simp only [encodeSubtype, dif_neg h0, val_ndrec] at h
State after:
case e_val.e_val.e_a.left.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⟩
h : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩

State before:
case e_val.e_val.e_a.left.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⟩
h : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Tactic:
cases h
State after:
case e_val.e_val.e_a.left.a.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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩

State before:
case e_val.e_val.e_a.left.a.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
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩
Tactic:
rfl
State after:
no goals

State before:
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
Tactic:
rfl
State after:
no goals