Inequalities · easy

Statement, exactly as the model and Lean see it

theorem lg_target (x : ℝ) : Real.cos x ^ 2 ≤ 1 := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 55

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified2 model calls · 2 Lean checks · $0.00022

Retrieved lemmas

1. Real.cos_sq_le_one
2. Real.one_sub_sq_div_two_le_cos
3. Real.cos_le_one_sub_mul_cos_sq
4. Real.cos_bound
5. Real.cos_sq'
6. Real.cos_sq
7. Real.cos_two_mul
8. Real.cos_two_mul'

Plan

### Explanation of the Proof: The theorem `lg_target` simply states that the square of the cosine of a real number is less than or equal to 1. This is a well-known inequality in trigonometry, and it can be directly proven using the identity `Real.cos_sq_le_one`, which is already provided in Mathlib. Thus, the proof is straightforward: we just need to apply this lemma directly. --- ### Lean Proof Skeleton: This skeleton uses a `have` statement to assert the desired inequality and then `exact this` to complete the proof.

Skeleton — Lean accepts it with only sorry steps left

have : Real.cos x ^ 2 ≤ 1 := Real.cos_sq_le_one x
exact this

Attempts

sample 0 · round 0Verified1.3 s model time
Proof
```
exact Real.cos_sq_le_one x
```

Verified proof

theorem lg_target (x : ℝ) : Real.cos x ^ 2 ≤ 1 := by
  exact Real.cos_sq_le_one x

Axioms used: propext, Classical.choice, Quot.sound

Reference proof

The proof we wrote and certified before any model ran.

nlinarith [Real.sin_sq_add_cos_sq x, sq_nonneg (Real.sin x)]