internlm/Lean-Github huggingface dataset:
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 : ⟨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]
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⟩
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'⟩
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 : ⟨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
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)
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'⟩
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)
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
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)
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'⟩
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)
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
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)
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
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)
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]
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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
Proof 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⟩
Theorem: Fin.specSigma
Proof 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)
Proof 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⟩
Theorem: Fin.specSigma
Proof 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
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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]
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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]
Proof 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⟩
Theorem: Fin.specSigma
Proof 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'
Proof 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⟩
Theorem: Fin.specSigma
Proof 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
Proof 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⟩
Theorem: Fin.specSigma
Proof 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 (.=.)
Proof 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⟩
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 : ⟨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]
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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
Proof 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
Theorem: Fin.specSigma
Proof 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
Proof state after:
no goals
Theorem: Fin.specSigma
Proof 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
Proof 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⟩
Theorem: Fin.specSigma
Proof 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
Proof 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
Theorem: Fin.specSigma
Proof 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]
Proof state after:
no goals