internlm/Lean-Github huggingface dataset:
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
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
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
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⟩
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⟩
h✝ : k < f 0
h : ⟨0, ⟨k, ⋯⟩⟩ = ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
⊢ encodeSigma f ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩ = ⟨k, hk⟩
Tactic:
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
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
Proof 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⟩
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⟩
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
Proof 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⟩
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⟩
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
Proof 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⟩
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⟩
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]
Proof 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
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⟩
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)
Proof 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
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⟩
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
Proof 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
Theorem: Fin.specSigma
Proof 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
Proof 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
Theorem: Fin.specSigma
Proof 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
Proof 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
Theorem: Fin.specSigma
Proof 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
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⟩
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]
Proof 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)
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⟩
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
Proof 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)
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
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
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⟩
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]
Proof 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⟩⟩
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⟩
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
Proof 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⟩⟩
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⟩
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
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
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⟩⟩
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
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
Proof 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
Theorem: Fin.specSigma
Proof 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
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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]
Proof 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