import Mathlib.Analysis.RCLike.Basic

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

/-
  Prove the following statement.

  A proof by cases is enough.
  You will not need any automated tactics here.
-/
example
  (α: Type)
  (P Q: α → Prop)
  (h1: ∀ a, P a ∨ Q a)
  (h2: ∀ a₁ a₂, P a₁ ∧ P a₂ → a₁ = a₂)
  (x y: α)
  : x=y ∨ (∃ a, Q a)
  := by
  sorry


/-
  Prove the following statement.

  Suggested main tactics and library results:
    - `induction` on ℕ
    - `calc` for a chain of inequalities
-/
#check zero_le
#check Order.add_one_le_iff

example
  (f: ℕ → ℕ)
  (f_monotonic: ∀ m, f m < f m.succ)
  : ∀ n, n ≤ f n
  := by
  sorry


/-
  Prove the following statement.

  Consider proving these equalities as intermediate steps:
    `f₁ x    + g₁ x    = f₂ x    + g₂ x   `
    `f₁ (-x) + g₁ (-x) = f₂ (-x) + g₂ (-x)`
    `f₁ x    - g₁ x    = f₂ x    - g₂ x   `

  You might need to use the tactic `change …` to rewrite
    `f x + g x`
  into
    `(f + g) x`
  and vice versa.
-/
#check add_left_cancel -- Might be useful.

def EvenFun (f: ℝ → ℝ): Prop := ∀ x, f (-x) = f x
def OddFun  (f: ℝ → ℝ): Prop := ∀ x, f (-x) = - f x

example
  (f₁ f₂ g₁ g₂: ℝ → ℝ)
  (f₁_even: EvenFun f₁)
  (f₂_even: EvenFun f₂)
  (g₁_odd: OddFun g₁)
  (g₂_odd: OddFun g₂)
  (eq_sum: f₁ + g₁ = f₂ + g₂)
  : f₁ = f₂ ∧ g₁ = g₂
  := by
  sorry


/-
  __Bonus__ exercise for extra credit.

  This is _not_ needed to achieve full marks. Feel free to skip this.
  I do not recommend you attempt this while you have not yet completed the
  previous exercises.

  You are _not_ truly expected to complete this in the given time.
  Provide a partial solution with `sorry`.

  Using Loogle is pretty much needed to search for useful library results.
  Use automation (`simp`, `grind`, …) aggressively.
-/
#check exists_rat_btwn

open Topology
example
  (f: ℝ → ℝ)
  (f_cont: Continuous f)
  (a b: ℝ)
  (h: ∀ x: ℚ, ↑x ∈ Set.Ioo a b → f x ≥ 0)  -- ≥0 on rationals
  : ∀ x ∈ Set.Ioo a b, f x ≥ 0             -- ≥0 on reals
  := by
  intro x hx
  by_contra f_neg
  simp at f_neg
  sorry