Theorem: IMOSL.IMO2006N3.g_succ (IMOSLLean4/IMO2006/N3/N3.lean)

State before:
n : ℕ
⊢ g n.succ = g n + n.succ.divisors.card
Tactic:
rw [g, g, Nat.divisors]
State after:
n : ℕ
⊢ ∑ k ∈ range n.succ, n.succ / (k + 1) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card

State before:
n : ℕ
⊢ ∑ k ∈ range n.succ, n.succ / (k + 1) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card
Tactic:
simp only [Nat.succ_div]
State after:
n : ℕ
⊢ ∑ x ∈ range n.succ, (n / (x + 1) + if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card

State before:
n : ℕ
⊢ ∑ x ∈ range n.succ, (n / (x + 1) + if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card
Tactic:
rw [card_filter, sum_Ico_eq_sum_range, Nat.add_sub_cancel, sum_add_distrib,
  sum_range_succ, Nat.div_eq_of_lt n.lt_succ_self]
State after:
n : ℕ
⊢ (∑ x ∈ range n, n / (x + 1) + 0 + ∑ x ∈ range n.succ, if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + ∑ k ∈ range n.succ, if 1 + k ∣ n.succ then 1 else 0

State before:
n : ℕ
⊢ (∑ x ∈ range n, n / (x + 1) + 0 + ∑ x ∈ range n.succ, if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + ∑ k ∈ range n.succ, if 1 + k ∣ n.succ then 1 else 0
Tactic:
exact congrArg₂ _ rfl (by simp only [add_comm 1])
State after:
no goals

State before:
n : ℕ
⊢ (∑ x ∈ range n.succ, if x + 1 ∣ n + 1 then 1 else 0) = ∑ k ∈ range n.succ, if 1 + k ∣ n.succ then 1 else 0
Tactic:
simp only [add_comm 1]
State after:
no goals