Theorem: Imo1979P1.lemma4 (Compfiles/Imo1979P1.lean)

State before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
have h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i =
          (∑ i ∈ Finset.Ico n (n + m), f i) +
          (∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i) := by
  have hmn : n ≤ n + m := Nat.le_add_right n m
  have hnk : n + m ≤ n + 2 * m := by omega
  exact (Finset.sum_Ico_consecutive (fun i ↦ f i) hmn hnk).symm
State after:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))

State before:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
rw [h1]
State after:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))

State before:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
clear h1
State after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))

State before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
simp only [Finset.sum_Ico_eq_sum_range, add_tsub_cancel_left]
State after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ x ∈ Finset.range m, f (n + x) + ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))

State before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ x ∈ Finset.range m, f (n + x) + ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
rw [Finset.sum_add_distrib, add_right_inj]
State after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))

State before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Tactic:
rw [show n + 2 * m - (n + m) = m by omega]
State after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))

State before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Tactic:
have h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i)) := by
  intro i hi
  rw [Finset.mem_range] at hi
  apply congr_arg
  omega
State after:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))

State before:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Tactic:
rw [Finset.sum_congr rfl h2]
State after:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))

State before:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))
Tactic:
let g i := f (n + m + i)
State after:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
g : ℕ → ℚ := fun i => f (n + m + i)
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))

State before:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
g : ℕ → ℚ := fun i => f (n + m + i)
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))
Tactic:
rw [Finset.sum_range_reflect g]
State after:
no goals

State before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Tactic:
have hmn : n ≤ n + m := Nat.le_add_right n m
State after:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i

State before:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Tactic:
have hnk : n + m ≤ n + 2 * m := by omega
State after:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
hnk : n + m ≤ n + 2 * m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i

State before:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
hnk : n + m ≤ n + 2 * m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Tactic:
exact (Finset.sum_Ico_consecutive (fun i ↦ f i) hmn hnk).symm
State after:
no goals

State before:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
⊢ n + m ≤ n + 2 * m
Tactic:
omega
State after:
no goals

State before:
n m : ℕ
f : ℕ → ℚ
⊢ n + 2 * m - (n + m) = m
Tactic:
omega
State after:
no goals

State before:
n m : ℕ
f : ℕ → ℚ
⊢ ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Tactic:
intro i hi
State after:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i ∈ Finset.range m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))

State before:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i ∈ Finset.range m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Tactic:
rw [Finset.mem_range] at hi
State after:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))

State before:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Tactic:
apply congr_arg
State after:
case h
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ n + (2 * m - 1 - i) = n + m + (m - 1 - i)

State before:
case h
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ n + (2 * m - 1 - i) = n + m + (m - 1 - i)
Tactic:
omega
State after:
no goals