Compfiles/Usa1996P1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1996, Problem 1

Prove that the average of the numbers n⬝sin(n π / 180) for n ∈ {2,4,6,…,180} is 1/tan(π/180).

Imports (4)
Imported by 1 file
  1. problem Usa1996P1.usa1996_p1 line 28 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Eq, Real, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Nat, Finset.sum, Finset.range, HAdd.hAdd, Real.sin, Real.pi, Real.tan

    Proof uses: Ne, Iff.mpr, Not, Iff.not, Real.sin_eq_zero_iff_of_lt_of_lt, lt_of_not_ge, Neg.neg, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 206 more

    180 instances, coercions and auxiliary constants left out.

    Tactic trace: 89 steps

    Open to load the checked before-and-after goal states.