Add random induction stuff

Changes

1 changed files (+36/-0)

• Induction.lean (new)
  • @@ -0,0 +1,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