import Mathlib.Analysis.RCLike.Basic
import Mathlib.Algebra.Module.LinearMap.Defs

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

/-
  Prove the following statement.
-/
example
  (α: Type)
  (P: α → Prop)
  (h: (∃ y, P y) ∧ (∀ a b, P a → P b → a = b))
  : ∃ c, ∀ x, P x ↔ x = c
  := by sorry


/-
  Prove the following statement.

  Suggested main tactics and library results:
    - `induction` on P
    - `convert_to` to rewrite goals in a different form
    - `ring` for general calculation
-/
#check dvd_add_self_right
#check dvd_mul_of_dvd_left

inductive P: ℤ → Prop
| base: P 4
| step1: ∀ a, P a → P (a + 8)
| step2: ∀ a, P a → P (a^2)

example
  (a: ℤ)
  (hn: P a)
  : 4 ∣ a
  := by sorry


/-
  Prove the following statement.

  No advanced tactics are needed. You can use the following basic results.
  You do not need anything else from the libraries.
-/
#check map_zero  -- Works on linear functions
#check zero_add

def affine₁
  {U V: Type}
  [AddCommGroup U] [AddCommGroup V] [Module ℝ U] [Module ℝ V]
  (f: U → V)
  := ∃ g: U →ₗ[ℝ] V, ∃ v₀: V, ∀ x, f x = g x + v₀

def affine₂
  {U V: Type}
  [AddCommGroup U] [AddCommGroup V] [Module ℝ U] [Module ℝ V]
  (f: U → V)
  := ∃ g: U →ₗ[ℝ] V, ∀ x, f x = g x + f 0

example
  {U V: Type}
  [AddCommGroup U] [AddCommGroup V] [Module ℝ U] [Module ℝ V]
  (f: U → V)
  : affine₁ f ↔ affine₂ f
  := 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.
  You can use all the available automation (`simp`, `grind`, …).
-/
open Topology
example
  (f g: ℝ → ℝ)
  (x yf yg: ℝ)
  (bound: f ≤ g) -- Pointwise ≤
  (hf: Filter.Tendsto f (𝓝[≠] x) (𝓝 yf))
  (hg: Filter.Tendsto g (𝓝[≠] x) (𝓝 yg))
  : yf ≤ yg
  := by sorry