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

State before:
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ f n < f n.succ
Tactic:
apply f_lt_f_of_g
State after:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ g n * n.succ < g n.succ * n

State before:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ g n * n.succ < g n.succ * n
Tactic:
rw [Nat.mul_succ, g_succ, add_mul, add_lt_add_iff_left, g_eq_sum_divisors_card]
State after:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∑ k ∈ range n, k.succ.divisors.card < n.succ.divisors.card * n

State before:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∑ k ∈ range n, k.succ.divisors.card < n.succ.divisors.card * n
Tactic:
calc _ < (range n).sum λ _ ↦ n.succ.divisors.card :=
      sum_lt_sum_of_nonempty (nonempty_range_iff.mpr h) (λ k h1 ↦ h0 k (mem_range.mp h1))
     _ = n.succ.divisors.card * n := by
      rw [sum_const, card_range, smul_eq_mul, mul_comm]
State after:
no goals

State before:
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∑ x ∈ range n, n.succ.divisors.card = n.succ.divisors.card * n
Tactic:
rw [sum_const, card_range, smul_eq_mul, mul_comm]
State after:
no goals