1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36

import Mathlib

example (n : ℕ) (h : 4 < n) : 69 * n + 42 < 2 * 3 ^ n + 4 := by
  induction h
  · norm_num
  · grind

example (n : ℕ) (h : 7 < n) : n + 1 < (4 / 3 : ℚ) ^ n := by
  induction h with
  | refl =>
    norm_num
  | step h ih =>
    -- have (a : ℚ) : a * a ^ n = a ^ (n + 1) := by
    --   grind
    grind


lemma blah (n x : ℕ) (h : x ≤ n) (f g : ℕ → ℕ) (hx : f x < g x) (hy : ∀ y ≥ x, g y * f (y + 1) < f y * g (y + 1)) : f n < g n := by
  induction h with
  | refl =>
    exact hx
  | step h ih =>
    simp at h
    rename_i m
    have h₁ := Nat.mul_lt_mul'' ih (hy m h)
    rw [← mul_assoc, ← mul_assoc, mul_comm (g m)] at h₁
    exact Nat.lt_of_mul_lt_mul_left h₁

example (n : ℕ) (h : 7 < n) : (n + 1) * 3 ^ n < 4 ^ n := by
  let f n := (n + 1) * 3 ^ n
  let g n := 4 ^ n
  have hy y (hy : y ≥ 8) : g y * f (y + 1) < f y * g (y + 1) := by
    suffices 3 * (y + 2) * (3 ^ y * 4 ^ y) < 4 * (y + 1) * (3 ^ y * 4 ^ y) by grind
    simp
    linarith
  exact blah n 8 h f g (by simp [f, g]) hy