Compfiles/Imo1966P4.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1966, Problem 4

Prove that for every natural number n and for every real number x that is not of the form kπ/2ᵗ for t a non-negative integer and k any integer,

1 / (sin 2x) + 1 / (sin 4x) + ... + 1 / (sin 2ⁿx) = cot x - cot 2ⁿ x.

Imports (3)
Imported by 1 file
  1. problem Imo1966P4.imo1966_p4 line 30 source

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

    Statement uses: Nat, Real, Int, Ne, HDiv.hDiv, HMul.hMul, Real.pi, HPow.hPow, OfNat.ofNat, Eq, Finset.sum, Finset.range, Real.sin, HAdd.hAdd, HSub.hSub, Real.cot

    Proof uses: Nat.recAux, Eq.mpr, EmptyCollection.emptyCollection, Finset, id, congrArg, Finset.range_zero, Finset.sum_empty, pow_zero, one_mul, sub_self, Eq.refl, Finset.sum_range_succ, Exists, False, Eq.mp, propext, Real.sin_eq_zero_iff, eq_div_iff, pow_ne_zero and 110 more

    140 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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