Compfiles/Usa1992P2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1992, Problem 2

Prove that

1 / cos 0° / cos 1° + 1 / cos 1° / cos 2° + ... + 1 / cos 88° / cos 99° = cos 1° / sin² 1°

Imports (4)
Imported by 1 file
  1. problem Usa1992P2.usa1992_p2 line 31 source

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

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

    Proof uses: LT.lt, Ne, Eq.mpr, Int, id, congrArg, propext, Real.cos_ne_zero_iff, Mathlib.Meta.NormNum.instAtLeastTwo, inferInstance, AddMonoidWithOne, Mathlib.Tactic.CancelDenoms.cancel_factors_ne, Mathlib.Tactic.CancelDenoms.div_subst, Mathlib.Tactic.CancelDenoms.mul_subst, rfl, Mul, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat and 109 more

    171 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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