-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
theorem rothNumberNat_le_ruzsaSzemerediNumberNat' :
    ∀ n : ℕ, (n / 3 - 2 : ℝ) * rothNumberNat ((n - 3) / 6) ≤ ruzsaSzemerediNumberNat n
  | 0 => by simp
  | 1 => by simp
  | 2 => by simp
  | n + 3 => by
    calc
      _ ≤ (↑(2 * (n / 6) + 1) : ℝ) * rothNumberNat (n / 6) :=
        mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
      _ ≤ (ruzsaSzemerediNumberNat (6 * (n / 6) + 3) : ℝ) := ?_
      _ ≤ _ :=
        Nat.cast_le.2 (ruzsaSzemerediNumberNat_mono <| add_le_add_right (Nat.mul_div_le _ _) _)
    · norm_num
      rw [← div_add_one (three_ne_zero' ℝ), ← le_sub_iff_add_le, div_le_iff₀ (zero_lt_three' ℝ),
        add_assoc, add_sub_assoc, add_mul, mul_right_comm]
      norm_num
      norm_cast
      rw [← mul_add_one]
      exact (Nat.lt_mul_div_succ _ <| by norm_num).le
    · norm_cast
      exact rothNumberNat_le_ruzsaSzemerediNumberNat _

Proof state:
case calc_1
n : ℕ
⊢ ↑(n + 3) / 3 - 2 ≤ ↑(2 * (n / 6) + 1)

Tactic:
norm_num

Result:
case calc_1
n : ℕ
⊢ (↑n + 3) / 3 ≤ 2 * ↑(n / 6) + 1 + 2

Proof state:
case calc_1
n : ℕ
⊢ n ≤ 6 * (n / 6 + 1)

Tactic:
exact (Nat.lt_mul_div_succ _ <| by norm_num).le

Result:
no goals

Proof state:
⊢ (↑0 / 3 - 2) * ↑(rothNumberNat ((0 - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat 0)

Tactic:
simp

Result:
no goals

Proof state:
⊢ (↑1 / 3 - 2) * ↑(rothNumberNat ((1 - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat 1)

Tactic:
simp

Result:
no goals

Proof state:
case calc_2
n : ℕ
⊢ (2 * (n / 6) + 1) * rothNumberNat (n / 6) ≤ ruzsaSzemerediNumberNat (6 * (n / 6) + 3)

Tactic:
exact rothNumberNat_le_ruzsaSzemerediNumberNat _

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < 6

Tactic:
norm_num

Result:
no goals

Proof state:
case calc_1
n : ℕ
⊢ ↑n ≤ 6 * ↑(n / 6) + 6

Tactic:
norm_cast

Result:
case calc_1
n : ℕ
⊢ n ≤ 6 * (n / 6) + 6

Proof state:
case calc_1
n : ℕ
⊢ ↑n ≤ 2 * 3 * ↑(n / 6) + (1 + 2 - 1) * 3

Tactic:
norm_num

Result:
case calc_1
n : ℕ
⊢ ↑n ≤ 6 * ↑(n / 6) + 6

Proof state:
case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))

Tactic:
norm_cast

Result:
case calc_2
n : ℕ
⊢ (2 * (n / 6) + 1) * rothNumberNat (n / 6) ≤ ruzsaSzemerediNumberNat (6 * (n / 6) + 3)

Proof state:
⊢ (↑2 / 3 - 2) * ↑(rothNumberNat ((2 - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat 2)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ (↑(n + 3) / 3 - 2) * ↑(rothNumberNat ((n + 3 - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat (n + 3))

Tactic:
calc
  _ ≤ (↑(2 * (n / 6) + 1) : ℝ) * rothNumberNat (n / 6) :=
    mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
  _ ≤ (ruzsaSzemerediNumberNat (6 * (n / 6) + 3) : ℝ) := ?_
  _ ≤ _ :=
    Nat.cast_le.2 (ruzsaSzemerediNumberNat_mono <| add_le_add_right (Nat.mul_div_le _ _) _)

Result:
case calc_1
n : ℕ
⊢ ↑(n + 3) / 3 - 2 ≤ ↑(2 * (n / 6) + 1)

case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))

Proof state:
case calc_1
n : ℕ
⊢ n ≤ 6 * (n / 6) + 6

Tactic:
rw [← mul_add_one]

Result:
case calc_1
n : ℕ
⊢ n ≤ 6 * (n / 6 + 1)

Proof state:
case calc_1
n : ℕ
⊢ (↑n + 3) / 3 ≤ 2 * ↑(n / 6) + 1 + 2

Tactic:
rw [← div_add_one (three_ne_zero' ℝ), ← le_sub_iff_add_le, div_le_iff₀ (zero_lt_three' ℝ),
  add_assoc, add_sub_assoc, add_mul, mul_right_comm]

Result:
case calc_1
n : ℕ
⊢ ↑n ≤ 2 * 3 * ↑(n / 6) + (1 + 2 - 1) * 3