mutable-state-inc/lean-collab/lean-syntax

-- WRONG
max(a, b)
min(x, y)
 
-- CORRECT
max a b
min x y

-- WRONG
x ∈ [0, π/2]
x ∈ (0, 1)
 
-- CORRECT
x ∈ Set.Icc 0 (Real.pi / 2)
x ∈ Set.Ioo 0 1

-- WRONG
x ∈ {y | P(y)}
 
-- CORRECT (simple predicate)
x ∈ {y | P y}
 
-- BETTER (avoid set-builder in goal types - decompose instead)
-- Instead of: x ∈ {c | ∀ y ∈ S, f c y}
-- Create separate goals:
--   1. "∀ y ∈ S, f x y" (the membership condition)
--   2. The remaining proof

--hypotheses "x : ℝ;;hx : x ∈ Set.Icc 0 Real.pi"

# WORKS - ;; delimiter handles internal commas
--hypotheses "c : ℝ;;hc : ∀ x ∈ Set.Icc 0 (Real.pi / 2), Real.sin x ≤ c * x"
 
# This correctly becomes TWO hypotheses:
#   1. c : ℝ
#   2. hc : ∀ x ∈ Set.Icc 0 (Real.pi / 2), Real.sin x ≤ c * x

-- WRONG (unmatched paren)
--hypotheses "h : (4 / Real.pi ^ 2) * (Real.pi - x) * x"
                                                      ^ missing close?
 
-- CORRECT
--hypotheses "h : (4 / Real.pi ^ 2) * (Real.pi - x) * x ≥ 0"

-- WRONG (causes syntax error)
--hypotheses ""
 
-- CORRECT (omit entirely for root goals)
./bin/lc create-goal --id "my-goal" --goal-type "P" --parent "root" --depth 1

-- Division
4 / Real.pi         -- division
(4 : ℝ) / Real.pi   -- explicit type annotation if needed
 
-- Powers
Real.pi ^ 2         -- pi squared
x ^ (1/2)           -- square root (or use Real.sqrt x)
Real.exp x          -- e^x
 
-- WRONG
π²
pi**2
 
-- CORRECT
Real.pi ^ 2

-- Goal type for IsGreatest
IsGreatest {c | ∀ x ∈ Set.Icc 0 (Real.pi / 2), c * x ≤ Real.sin x} (2 / Real.pi)
 
-- After `constructor`, children are:
-- 1. Membership: (2 / Real.pi) ∈ {c | ∀ x ∈ ..., c * x ≤ Real.sin x}
-- 2. Upper bound: ∀ c ∈ {c | ...}, c ≤ 2 / Real.pi

-- Parent: ∀ x ∈ Set.Icc 0 (Real.pi / 2), P x
-- After `intro x hx`:
-- Child goal: P x
-- Child hypotheses: "x : ℝ,hx : x ∈ Set.Icc 0 (Real.pi / 2)"

-- Parent: P ∧ Q
-- After `constructor`:
-- Child 1: P
-- Child 2: Q
-- (hypotheses inherited from parent)

# 1. ALWAYS try suggest first
./bin/lc suggest --goal $GOAL_ID
 
# 2. Search for similar patterns
./bin/lc search "sphere infinite" --prefix tactics/
 
# 3. Check the actual Mathlib namespace (in Lean REPL)
#check @Metric.sphere_infinite  -- see the real signature

-- Trigonometric
Real.sin x, Real.cos x, Real.tan x
 
-- Arithmetic
a + b, a - b, a * b, a / b, a ^ n
 
-- Comparisons
a ≤ b, a < b, a = b, a ≠ b
 
-- Logic
P ∧ Q, P ∨ Q, P → Q, ¬P
 
-- Quantifiers (in goal types)
∀ x, P x
∀ x ∈ S, P x
∃ x, P x
 
-- Sets
x ∈ S
Set.Icc a b  -- [a, b]
Set.Ioo a b  -- (a, b)
 
-- Special structures
IsGreatest S x
IsLeast S x
ConcaveOn ℝ S f
ConvexOn ℝ S f