Compfiles/Imo1963P5.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1963, Problem 5

Prove that cos(π/7) - cos(2π/7) + cos(3π/7) = 1/2.

Imports (4)
Imported by 1 file
  1. problem Imo1963P5.imo1963_p5 line 29 source

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

    Statement uses: Eq, Real, HAdd.hAdd, HSub.hSub, Real.cos, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, HMul.hMul

    Proof uses: Eq.mpr, id, congrArg, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 124 more

    137 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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