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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
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⟩
Tactic:
next => cases h
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
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⟩

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⟩
h✝ : k < f 0
h : ⟨0, ⟨k, ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
cases h
State after:
no goals

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⟩
hge : ¬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⟩
Tactic:
have hge := Nat.ge_of_not_lt hge
State after:
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
have hpos : 0 < sum (f ∘ succ) := by
  apply Nat.pos_of_nonzero
  intro hz
  rw [Fin.sum_succ, hz] at hk
  contradiction
State after:
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
have hk' : k - f 0 < sum (f ∘ succ) := by
  rw [Nat.sub_lt_iff_lt_add_of_pos _ _ _ hpos]
  rw [sum_succ] at hk
  exact hk
State after:
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
simp [encodeSigma]
State after:
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = k

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = k
Tactic:
transitivity (f 0 + (encodeSigma (f ∘ succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, ⟨j, hj⟩⟩).val)
State after:
case left
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩)

case right
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = k

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
⊢ 0 < sum (f ∘ succ)
Tactic:
apply Nat.pos_of_nonzero
State after:
case a
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
⊢ sum (f ∘ succ) ≠ 0

State before:
case a
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
⊢ sum (f ∘ succ) ≠ 0
Tactic:
intro hz
State after:
case a
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False

State before:
case a
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False
Tactic:
rw [Fin.sum_succ, hz] at hk
State after:
case a
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
hk : k < f 0 + 0
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False

State before:
case a
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
hk : k < f 0 + 0
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False
Tactic:
contradiction
State after:
no goals

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k - f 0 < sum (f ∘ succ)
Tactic:
rw [Nat.sub_lt_iff_lt_add_of_pos _ _ _ hpos]
State after:
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)
Tactic:
rw [sum_succ] at hk
State after:
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
hk : k < f 0 + sum (f ∘ succ)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)

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
hk : k < f 0 + sum (f ∘ succ)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)
Tactic:
exact hk
State after:
no goals

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
Tactic:
rw [←ih]
State after:
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩

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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
Tactic:
injection h with h1 h2
State after:
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⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
h1 : ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ⟨i + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩

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⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
h1 : ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ⟨i + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
Tactic:
cases h1
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1, ⋯⟩, ⟨j, hj⟩⟩

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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1, ⋯⟩, ⟨j, hj⟩⟩
Tactic:
apply Sigma.eq
State after:
case refl.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1, ⋯⟩, ⟨j, hj⟩⟩.fst

case refl.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd ≅ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1, ⋯⟩, ⟨j, hj⟩⟩.snd

State before:
case refl.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1, ⋯⟩, ⟨j, hj⟩⟩.fst
Tactic:
rfl
State after:
no goals

State before:
case refl.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd ≅ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1, ⋯⟩, ⟨j, hj⟩⟩.snd
Tactic:
exact h2
State after:
no goals

State before:
case left
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩)
Tactic:
rfl
State after:
no goals

State before:
case right
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = k
Tactic:
rw [this]
State after:
case right
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑⟨k - f 0, hk'⟩ = k

State before:
case right
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 + ↑⟨k - f 0, hk'⟩ = k
Tactic:
rw [Nat.add_comm, Nat.sub_add_cancel]
State after:
case right
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 ≤ k

State before:
case right
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⟩
hge✝ : ¬k < f 0
h :
  ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
⊢ f 0 ≤ k
Tactic:
exact hge
State after:
no goals

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
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⟩⟩
Tactic:
intro h
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
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

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
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
⊢ decodeSigma f ⟨k, hk⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
simp only [decodeSigma]
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
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
⊢ (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⟩⟩

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
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
⊢ (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⟩⟩
Tactic:
simp only [encodeSigma] at h
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
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
⊢ (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⟩⟩

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
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
⊢ (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⟩⟩
Tactic:
split
State after:
case mpr.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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
h✝ : k < f 0
⊢ ⟨0, ⟨k, ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

case mpr.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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
h✝ : ¬k < f 0
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

State before:
case mpr.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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
h✝ : k < f 0
⊢ ⟨0, ⟨k, ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

case mpr.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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
h✝ : ¬k < f 0
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
next hlt =>
  cases h
  absurd hlt
  apply Nat.not_lt_of_ge
  exact Nat.le_add_right ..
State after:
case mpr.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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
h✝ : ¬k < f 0
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hlt : k < f 0
⊢ ⟨0, ⟨k, ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
cases h
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hlt : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
⊢ ⟨0, ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hlt : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
⊢ ⟨0, ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
absurd hlt
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hlt : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
⊢ ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0

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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hlt : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
⊢ ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
Tactic:
apply Nat.not_lt_of_ge
State after:
case refl.a
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hlt : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0

State before:
case refl.a
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hlt : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
⊢ f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
Tactic:
exact Nat.le_add_right ..
State after:
no goals

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge : ¬k < f 0
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
have hge := Nat.ge_of_not_lt hge
State after:
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
have hpos : 0 < sum (f ∘ succ) := by
  apply Nat.pos_of_nonzero
  intro hz
  rw [sum_succ, hz] at hk
  contradiction
State after:
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
have hk' : k - f 0 < sum (f ∘ succ) := by
  rw [Nat.sub_lt_iff_lt_add_of_pos _ _ _ hpos]
  rw [sum_succ] at hk
  exact hk
State after:
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
have : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, ⟨j,hj⟩⟩ := by
  rw [ih]
  cases h
  apply Fin.eq
  clean
  rw [Nat.add_sub_cancel_left]
State after:
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
Tactic:
congr 1
State after:
case h.e_3.h
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ⟨i + 1, hi⟩

case h.e_4
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
⊢ 0 < sum (f ∘ succ)
Tactic:
apply Nat.pos_of_nonzero
State after:
case a
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
⊢ sum (f ∘ succ) ≠ 0

State before:
case a
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
⊢ sum (f ∘ succ) ≠ 0
Tactic:
intro hz
State after:
case a
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False

State before:
case a
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False
Tactic:
rw [sum_succ, hz] at hk
State after:
case a
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
hk : k < f 0 + 0
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk✝⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False

State before:
case a
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
hk : k < f 0 + 0
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk✝⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hz : sum (f ∘ succ) = 0
⊢ False
Tactic:
contradiction
State after:
no goals

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k - f 0 < sum (f ∘ succ)
Tactic:
rw [Nat.sub_lt_iff_lt_add_of_pos _ _ _ hpos]
State after:
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)
Tactic:
rw [sum_succ] at hk
State after:
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
hk : k < f 0 + sum (f ∘ succ)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk✝⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)

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
hk : k < f 0 + sum (f ∘ succ)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk✝⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
⊢ k < f 0 + sum (f ∘ succ)
Tactic:
exact hk
State after:
no goals

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
Tactic:
rw [ih]
State after:
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
⊢ encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨k - f 0, hk'⟩
Tactic:
cases h
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hpos : 0 < sum (f ∘ succ)
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hge✝ : ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
hge : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
hk' : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0 < sum (f ∘ succ)
⊢ encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0, hk'⟩

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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hpos : 0 < sum (f ∘ succ)
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hge✝ : ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
hge : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
hk' : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0 < sum (f ∘ succ)
⊢ encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩ = ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0, hk'⟩
Tactic:
apply Fin.eq
State after:
case refl.a
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hpos : 0 < sum (f ∘ succ)
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hge✝ : ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
hge : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
hk' : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0 < sum (f ∘ succ)
⊢ ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = ↑⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0, hk'⟩

State before:
case refl.a
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hpos : 0 < sum (f ∘ succ)
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hge✝ : ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
hge : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
hk' : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0 < sum (f ∘ succ)
⊢ ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = ↑⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0, hk'⟩
Tactic:
clean
State after:
case refl.a
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hpos : 0 < sum (f ∘ succ)
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hge✝ : ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
hge : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
hk' : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0 < sum (f ∘ succ)
⊢ ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0

State before:
case refl.a
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hpos : 0 < sum (f ∘ succ)
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hge✝ : ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
hge : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
hk' : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0 < sum (f ∘ succ)
⊢ ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0
Tactic:
rw [Nat.add_sub_cancel_left]
State after:
no goals

State before:
case h.e_3.h
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ⟨i + 1, hi⟩
Tactic:
apply Fin.eq
State after:
case h.e_3.h.a
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ↑⟨i + 1, hi⟩

State before:
case h.e_3.h.a
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ↑⟨i + 1, hi⟩
Tactic:
transitivity ((decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).1.1+1)
State after:
case h.e_3.h.a.left
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1

case h.e_3.h.a.right
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 = ↑⟨i + 1, hi⟩

State before:
case h.e_3.h.a.left
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1
Tactic:
rfl
State after:
no goals

State before:
case h.e_3.h.a.right
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 = ↑⟨i + 1, hi⟩
Tactic:
rw [this]
State after:
no goals

State before:
case h.e_4
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
Tactic:
have t' : (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst.val = i := by
  rw [this]
State after:
case h.e_4
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
t' : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst = i
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩

State before:
case h.e_4
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 : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
t' : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst = i
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
Tactic:
cases t'
State after:
case h.e_4.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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩

State before:
case h.e_4.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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
Tactic:
apply heq_of_eq
State after:
case h.e_4.refl.h
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd = ⟨j, hj⟩

State before:
case h.e_4.refl.h
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd = ⟨j, hj⟩
Tactic:
transitivity ((decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).2) using (.=.)
State after:
case h.e_4.refl.h.left
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd = (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd

case h.e_4.refl.h.right
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd = ⟨j, hj⟩

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⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst = i
Tactic:
rw [this]
State after:
no goals

State before:
case h.e_4.refl.h.left
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd = (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd
Tactic:
apply Fin.eq
State after:
case h.e_4.refl.h.left.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd = ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd

State before:
case h.e_4.refl.h.left.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd = ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd
Tactic:
rfl
State after:
no goals

State before:
case h.e_4.refl.h.right
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd = ⟨j, hj⟩
Tactic:
apply Fin.eq
State after:
case h.e_4.refl.h.right.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd = ↑⟨j, hj⟩

State before:
case h.e_4.refl.h.right.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd = ↑⟨j, hj⟩
Tactic:
clean
State after:
case h.e_4.refl.h.right.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd = j

State before:
case h.e_4.refl.h.right.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst, ⋯⟩, ⟨j, hj⟩⟩
⊢ ↑(decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).snd = j
Tactic:
rw [this]
State after:
no goals