mutable-state-inc/lean-collab/mathlib-knowledge

Real.sin_zero : sin 0 = 0
Real.sin_pi : sin π = 0
Real.cos_zero : cos 0 = 1
Real.cos_pi : cos π = -1
Real.sin_nonneg_of_mem_Icc : x ∈ Icc 0 π → 0 ≤ sin x
Real.sin_pos_of_mem_Ioo : x ∈ Ioo 0 π → 0 < sin x
Real.sin_le_one : sin x ≤ 1
Real.neg_one_le_sin : -1 ≤ sin x

Real.exp_zero : exp 0 = 1
Real.exp_pos : 0 < exp x
Real.exp_lt_exp : exp x < exp y ↔ x < y
Real.log_exp : log (exp x) = x
Real.exp_log (h : 0 < x) : exp (log x) = x
Real.log_mul (hx : 0 < x) (hy : 0 < y) : log (x * y) = log x + log y
Real.log_one : log 1 = 0
Real.log_lt_log (hx : 0 < x) : log x < log y ↔ x < y

Real.pi_pos : 0 < π
Real.pi_gt_three : 3 < π
Real.pi_lt_four : π < 4
Real.two_le_pi : 2 ≤ π

-- AM-GM (Arithmetic-Geometric Mean)
add_div_two_ge_sqrt_mul (ha : 0 ≤ a) (hb : 0 ≤ b) :
  (a + b) / 2 ≥ √(a * b)
 
-- Cauchy-Schwarz
inner_mul_le_norm_mul_norm : |⟪x, y⟫| ≤ ‖x‖ * ‖y‖
 
-- Triangle Inequality
norm_add_le : ‖x + y‖ ≤ ‖x‖ + ‖y‖
abs_add : |a + b| ≤ |a| + |b|

sq_nonneg x : 0 ≤ x^2                    -- ALWAYS use this
sq_abs x : |x|^2 = x^2
sq_le_sq' (h1 : -a ≤ b) (h2 : b ≤ a) : b^2 ≤ a^2
mul_self_nonneg : 0 ≤ a * a
add_pow_le_pow_mul_pow_of_sq_le_sq       -- for (a+b)^n bounds

mul_le_mul_of_nonneg_left (h : b ≤ c) (a0 : 0 ≤ a) : a * b ≤ a * c
mul_le_mul_of_nonneg_right (h : b ≤ c) (a0 : 0 ≤ a) : b * a ≤ c * a
div_le_div_of_nonneg_left (h : b ≤ c) (a0 : 0 ≤ a) (c0 : 0 < c) : a / c ≤ a / b

-- If f is concave on [a,b], then f lies ABOVE the secant line
ConcaveOn.le_right_of_lt_left (hf : ConcaveOn ℝ (Icc a b) f)
  (ha : a < x) (hx : x ≤ b) :
  f x ≥ f a + (f b - f a) / (b - a) * (x - a)
 
-- If f is convex, then f lies BELOW the secant line
ConvexOn.le_left_of_lt_right (hf : ConvexOn ℝ (Icc a b) f)
  (hx : a ≤ x) (xb : x < b) :
  f x ≤ f a + (f b - f a) / (b - a) * (x - a)

strictConcaveOn_sin_Icc : StrictConcaveOn ℝ (Icc 0 π) sin
strictConcaveOn_cos_Icc : StrictConcaveOn ℝ (Icc (-π/2) (π/2)) cos
strictConvexOn_exp : StrictConvexOn ℝ univ exp
strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log

-- sin is concave on [0,π], so sin x ≥ secant line from (0,0) to (π,0)
-- The secant is y = 0, not useful
-- Better: secant from (0,0) to (π/2, 1) gives sin x ≥ (2/π)x on [0,π/2]
-- This is the "Jordan's inequality" technique

-- Membership
Set.mem_Icc : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b
Set.mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b
Set.mem_Ico : x ∈ Ico a b ↔ a ≤ x ∧ x < b
 
-- Subset relations
Ioo_subset_Icc_self : Ioo a b ⊆ Icc a b
Icc_subset_Icc (h1 : a' ≤ a) (h2 : b ≤ b') : Icc a b ⊆ Icc a' b'
 
-- Endpoints
left_mem_Icc : a ∈ Icc a b ↔ a ≤ b
right_mem_Icc : b ∈ Icc a b ↔ a ≤ b

Nat.prime_def_lt : p.Prime ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1
Nat.Prime.one_lt : p.Prime → 1 < p
Nat.Prime.ne_one : p.Prime → p ≠ 1
Nat.exists_prime_and_dvd (h : 2 ≤ n) : ∃ p, p.Prime ∧ p ∣ n
Nat.factors_prime : p ∈ n.factors → p.Prime

Goal: f(a) ≤ f(b) where a ≤ b
 
Strategy:
1. Find/prove: Monotone f (or MonotoneOn f S)
2. Apply: Monotone.le_of_le or MonotoneOn.le_of_le

Goal: f(x) ≤ g(x) where g is linear
 
Strategy:
1. Check: Is f convex? Then f ≤ secant line
2. Check: Is f concave? Then f ≥ secant line
3. Use: ConvexOn.le_right or ConcaveOn.le_right

Goal: a ≤ f(x) ≤ b
 
Strategy:
1. Find intermediate: a ≤ g(x) ≤ f(x) or f(x) ≤ h(x) ≤ b
2. Chain with: le_trans, lt_of_le_of_lt, lt_of_lt_of_le

Goal: f(x) = c
 
Strategy:
1. Prove: f(x) ≤ c (upper bound)
2. Prove: c ≤ f(x) (lower bound)
3. Apply: le_antisymm

Goal: 0 < f(x)
 
Strategy:
1. If product: mul_pos h1 h2
2. If sum of positives: add_pos h1 h2
3. If square: sq_pos_of_ne_zero h
4. If exponential: exp_pos x
5. If specific: pi_pos, one_pos, etc.

Goal: sin x ≤ polynomial(x) on interval
 
Strategy:
1. Use concavity: sin is concave on [0,π]
2. Compare to secant line between key points
3. Apply: strictConcaveOn_sin_Icc.concaveOn.le_right
4. Compute: endpoint values to verify secant bound

-- Basic pattern
nlinarith [sq_nonneg x, sq_nonneg y, h1, h2]
 
-- Common hints to include:
sq_nonneg x          -- x^2 ≥ 0
sq_nonneg (x - y)    -- (x-y)^2 ≥ 0, expands to x^2 - 2xy + y^2 ≥ 0
mul_self_nonneg x    -- x * x ≥ 0
sq_abs x             -- |x|^2 = x^2
abs_nonneg x         -- 0 ≤ |x|
 
-- From hypotheses
mul_nonneg h1 h2     -- if h1 : 0 ≤ a, h2 : 0 ≤ b, then 0 ≤ a*b
mul_pos h1 h2        -- if h1 : 0 < a, h2 : 0 < b, then 0 < a*b

example : IsLeast S x := by
  constructor
  · -- Membership: x ∈ S
    simp [S]  -- or exact ⟨_, _⟩
  · -- Minimality: ∀ y ∈ S, x ≤ y
    intro y hy
    obtain ⟨hy1, hy2⟩ := hy
    nlinarith  -- or omega, linarith

example : ∀ x ∈ Icc a b, P x := by
  intro x hx
  obtain ⟨ha, hb⟩ := hx  -- ha : a ≤ x, hb : x ≤ b
  -- now prove P x using ha, hb

example : ∃ x ∈ S, P x := by
  use 42        -- the witness
  constructor
  · norm_num    -- 42 ∈ S
  · ring        -- P 42

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -- sin, cos
import Mathlib.Analysis.SpecialFunctions.Exp -- exp, log
import Mathlib.Analysis.SpecialFunctions.Pow.Real -- rpow
import Mathlib.Analysis.Convex.SpecificFunctions.Basic -- convexity of exp, etc.
import Mathlib.Analysis.MeanInequalities -- AM-GM, etc.
import Mathlib.Order.Bounds.Basic -- IsLeast, IsGreatest
import Mathlib.Topology.Order.Basic -- continuity + order

GOAL                          TACTIC
────────────────────────────────────────
0 < 5                         norm_num
x + y = y + x                 ring
a ≤ b → b ≤ c → a ≤ c        exact le_trans h1 h2
0 ≤ x^2                       exact sq_nonneg x
x ∈ Icc 0 1                   exact ⟨by norm_num, by norm_num⟩
P ∧ Q                         exact ⟨hP, hQ⟩  or  constructor
∃ x, P x                      exact ⟨witness, proof⟩  or  use witness
sin x ≤ 1                     exact Real.sin_le_one x
0 < π                         exact Real.pi_pos
exp 0 = 1                     exact Real.exp_zero
f concave, bound needed       ConcaveOn.le_right ...
x^2 + y^2 ≥ 0                 nlinarith [sq_nonneg x, sq_nonneg y]