internlm/Lean-Github huggingface dataset:
Theorem: Fin.specFun
Proof state before:
case refl.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (encodeFun fun k => x k.succ).decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
rw [ih1]
Proof state after:
case refl.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (fun k => x k.succ) ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Theorem: Fin.specFun
Proof state before:
case refl.right
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : ↑(x 0) + n * ↑(encodeFun fun k => x k.succ) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
this : ↑(encodeFun fun k => x k.succ) = k / n
⊢ (fun k => x k.succ) ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
case zero
f : Fin 0 → Nat
k : Fin (sum f)
x : (i : Fin 0) × Fin (f i)
⊢ decodeSigma f k = x ↔ encodeSigma f x = k
Tactic:
match k, x with | ⟨_, h⟩, _ => simp [sum] at h; contradiction
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
f : Fin 0 → Nat
k : Fin (sum f)
x : (i : Fin 0) × Fin (f i)
val✝ : Nat
h : val✝ < sum f
x✝ : (i : Fin 0) × Fin (f i)
⊢ decodeSigma f ⟨val✝, h⟩ = x✝ ↔ encodeSigma f x✝ = ⟨val✝, h⟩
Tactic:
simp [sum] at h
Proof state after:
f : Fin 0 → Nat
k : Fin (sum f)
x : (i : Fin 0) × Fin (f i)
val✝ : Nat
h : val✝ < 0
x✝ : (i : Fin 0) × Fin (f i)
⊢ decodeSigma f ⟨val✝, h⟩ = x✝ ↔ encodeSigma f x✝ = ⟨val✝, h⟩
Theorem: Fin.specSigma
Proof state before:
f : Fin 0 → Nat
k : Fin (sum f)
x : (i : Fin 0) × Fin (f i)
val✝ : Nat
h : val✝ < 0
x✝ : (i : Fin 0) × Fin (f i)
⊢ decodeSigma f ⟨val✝, h⟩ = x✝ ↔ encodeSigma f x✝ = ⟨val✝, h⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ ↔ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
constructor
Proof state after:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ → encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩

case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩ → decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
Theorem: Fin.specSigma
Proof state before:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ → encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
intro h
Proof state after:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h : decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Theorem: Fin.specSigma
Proof state before:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h : decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
unfold decodeSigma at h
Proof state after:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h :
  (if hk0 : k < f 0 then ⟨0, ⟨k, hk0⟩⟩
    else
      let_fun hpos := ⋯;
      let_fun hkf := ⋯;
      match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
      | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Theorem: Fin.specSigma
Proof state before:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h :
  (if hk0 : k < f 0 then ⟨0, ⟨k, hk0⟩⟩
    else
      let_fun hpos := ⋯;
      let_fun hkf := ⋯;
      match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
      | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
split at h
Proof state after:
case mp.isTrue
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : k < f 0
h : ⟨0, ⟨k, h✝⟩⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩

case mp.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
h :
  (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Theorem: Fin.specSigma
Proof state before:
case mp.isTrue
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : k < f 0
h : ⟨0, ⟨k, h✝⟩⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩

case mp.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
h :
  (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
next => cases h; rfl
Proof state after:
case mp.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
h :
  (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Theorem: Fin.specSigma
Proof state before:
case mp.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
h :
  (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
next => cases h
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : k < f 0
h : ⟨0, ⟨k, h✝⟩⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
cases h
Proof state after:
case refl
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
h✝ : k < f 0
isLt✝ : k < f ⟨0, isLt✝¹⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩ = ⟨k, hk⟩
Theorem: Fin.specSigma
Proof state before:
case refl
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
h✝ : k < f 0
isLt✝ : k < f ⟨0, isLt✝¹⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
h :
  (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
Tactic:
cases h
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
⊢ encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩ → decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
Tactic:
intro h
Proof state after:
case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h : encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
Theorem: Fin.specSigma
Proof state before:
case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h : encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
Tactic:
unfold decodeSigma
Proof state after:
case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h : encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
⊢ (if hk0 : k < f 0 then ⟨0, ⟨k, hk0⟩⟩
    else
      let_fun hpos := ⋯;
      let_fun hkf := ⋯;
      match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
      | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
Theorem: Fin.specSigma
Proof state before:
case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
val✝ : Nat
isLt✝ : val✝ < f ⟨0, isLt✝¹⟩
h : encodeSigma f ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩ = ⟨k, hk⟩
⊢ (if hk0 : k < f 0 then ⟨0, ⟨k, hk0⟩⟩
    else
      let_fun hpos := ⋯;
      let_fun hkf := ⋯;
      match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
      | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨val✝, isLt✝⟩⟩
Tactic:
cases h
Proof state after:
case mpr.refl
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
⊢ (if hk0 : k < f 0 then ⟨0, ⟨k, hk0⟩⟩
    else
      let_fun hpos := ⋯;
      let_fun hkf := ⋯;
      match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
      | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Theorem: Fin.specSigma
Proof state before:
case mpr.refl
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
⊢ (if hk0 : k < f 0 then ⟨0, ⟨k, hk0⟩⟩
    else
      let_fun hpos := ⋯;
      let_fun hkf := ⋯;
      match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
      | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Tactic:
split
Proof state after:
case mpr.refl.isTrue
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : k < f 0
⊢ ⟨0, ⟨k, h✝⟩⟩ = ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩

case mpr.refl.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
⊢ (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Theorem: Fin.specSigma
Proof state before:
case mpr.refl.isTrue
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : k < f 0
⊢ ⟨0, ⟨k, h✝⟩⟩ = ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩

case mpr.refl.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
⊢ (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Tactic:
next => rfl
Proof state after:
case mpr.refl.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
⊢ (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Theorem: Fin.specSigma
Proof state before:
case mpr.refl.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
⊢ (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Tactic:
next => contradiction
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : k < f 0
⊢ ⟨0, ⟨k, h✝⟩⟩ = ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
isLt✝¹ : 0 < n + 1
isLt✝ : k < f ⟨0, isLt✝¹⟩
h✝ : ¬k < f 0
⊢ (let_fun hpos := ⋯;
    let_fun hkf := ⋯;
    match decodeSigma (f ∘ succ) ⟨k - f 0, hkf⟩ with
    | ⟨⟨i, hi⟩, j⟩ => ⟨⟨i + 1, ⋯⟩, j⟩) =
    ⟨⟨0, isLt✝¹⟩, ⟨k, isLt✝⟩⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.specSigma
Proof state before:
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ ↔ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
constructor
Proof state after:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ → encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩

case mpr
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩ → decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Theorem: Fin.specSigma
Proof state before:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ → encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
intro h
Proof state after:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Theorem: Fin.specSigma
Proof state before:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
simp only [decodeSigma] at h
Proof state after:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h :
  (if h : k < f 0 then ⟨0, ⟨k, ⋯⟩⟩
    else ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩) =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Theorem: Fin.specSigma
Proof state before:
case mp
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h :
  (if h : k < f 0 then ⟨0, ⟨k, ⋯⟩⟩
    else ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩) =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
split at h
Proof state after:
case mp.isTrue
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h✝ : k < f 0
h : ⟨0, ⟨k, ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩

case mp.isFalse
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩