Compfiles/Usa1980P3.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1980, Problem 3

A + B + C is an integral multiple of π. x, y, z are real numbers. If x sin A + y sin B + z sin C = x^2 sin 2A + y^2 sin 2B + z^2 sin 2C = 0, show that x^n sin nA + y^n sin n^B + z^n sin nC = 0 for any positive integer n.

Imports (2)
Imported by 1 file
  1. abbrev P line 36 source

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

    Statement uses: Nat, MvPolynomial, Fin, OfNat.ofNat, Complex

    Proof uses: MvPolynomial.psum

    5 instances, coercions and auxiliary constants left out.

  2. abbrev S line 38 source

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

    Statement uses: Nat, MvPolynomial, Fin, OfNat.ofNat, Complex

    Proof uses: MvPolynomial.esymm

    5 instances, coercions and auxiliary constants left out.

  3. def f line 40 source

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

    Statement uses: Real, Fin, OfNat.ofNat, Nat, Complex

    Proof uses: f.match_1, Unit, HMul.hMul, Complex.exp, Complex.I

    5 instances, coercions and auxiliary constants left out.

  4. lemma movire line 49 source

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

    Statement uses: Nat, Complex, Eq, HPow.hPow, Complex.exp, HMul.hMul, Complex.I

    Proof uses: Eq.mp, HAdd.hAdd, Complex.cos, Complex.sin, congr, congrArg, congrFun', Complex.cos_add_sin_I, Complex.cos_add_sin_mul_I_pow

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. lemma P_def line 52 source

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

    Statement uses: Nat, Eq, MvPolynomial, Fin, OfNat.ofNat, Complex, P, HAdd.hAdd, Finsupp, HPow.hPow, MvPolynomial.X

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Fin.sum_univ_three, eq_self

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  6. lemma prod_f_im line 55 source

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

    Statement uses: Real, Exists, Int, Eq, HAdd.hAdd, HMul.hMul, Real.pi, Complex.im, Finset.prod, Fin, OfNat.ofNat, Nat, Complex, Finset.univ, f

    Proof uses: Iff.mp, LE.le, Complex.partialOrder, HPow.hPow, Complex.sq_nonneg_iff, Eq.mpr, Complex.exp, Complex.I, id, congrArg, congrFun', Fin.prod_univ_three, f.match_1, Unit, of_eq_true, Eq.trans, inferInstance, CommGroupWithZero, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq and 49 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  7. lemma sum_f_im line 72 source

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

    Statement uses: Real, Eq, HAdd.hAdd, HMul.hMul, Real.sin, OfNat.ofNat, Complex.im, Finset.sum, Fin, Nat, Complex, Finset.univ, f

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Complex.exp, Complex.I, Fin.sum_univ_three, f.match_1, Unit, congr, Complex.re, Complex.mul_im, Complex.exp_ofReal_mul_I_im, Real.cos, Complex.exp_ofReal_mul_I_re, MulZeroClass.zero_mul, add_zero, eq_self

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma S_two line 75 source

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

    Statement uses: Eq, MvPolynomial, Fin, OfNat.ofNat, Nat, Complex, S, HMul.hMul, Finsupp, RingHom, MvPolynomial.C, HDiv.hDiv, HSub.hSub, P

    Proof uses: of_eq_true, Eq.trans, True, implies_congr, Or, False, congrArg, or_false, Eq.refl, Finset, Prod, Finset.filter, LT.lt, Prod.fst, Finset.HasAntidiagonal.antidiagonal, Insert.insert, Prod.mk, Singleton.singleton, Eq.mpr, Finset.map and 62 more

    202 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  9. lemma S_more line 83 source

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

    Statement uses: Nat, Eq, MvPolynomial, Fin, OfNat.ofNat, Complex, S, HAdd.hAdd, Finsupp

    Proof uses: Finset, Finset.powersetCard, Finset.univ, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, LT.lt, Finset.card, True, congrFun', congrArg, Fintype.card_fin, Function.swap, LE.le, Finset.sum_congr, Finset.prod, MvPolynomial.X, Membership.mem, Eq.refl, eq_self

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  10. lemma P_iff line 87 source

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

    Statement uses: Real, Nat, Iff, Eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Real.sin, OfNat.ofNat, Complex.im, RingHom, MvPolynomial, Fin, Complex, Finsupp, MvPolynomial.eval, f, P

    Proof uses: Eq.mpr, Complex.re, Complex.exp, Complex.I, id, congrArg, congrFun', Eq.trans, MvPolynomial.X, P_def, map_add, congr, map_pow, MvPolynomial.eval_X, mul_pow, movire, Complex.mul_im, Eq.symm, Nat.cast_zero, Complex.ofReal_mul and 6 more

    86 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  11. lemma P_three line 95 source

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

    Statement uses: Eq, MvPolynomial, Fin, OfNat.ofNat, Nat, Complex, P, HAdd.hAdd, Finsupp, HSub.hSub, HMul.hMul, S

    Proof uses: MvPolynomial.esymm, HPow.hPow, Neg.neg, Finset.sum, Prod, Finset.filter, LT.lt, Prod.fst, Finset.HasAntidiagonal.antidiagonal, MvPolynomial.psum, Prod.snd, MvPolynomial.mul_esymm_eq_sum, Finset, Insert.insert, Prod.mk, Singleton.singleton, Eq.mpr, Finset.image, Finset.range, id and 94 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  12. lemma P_more line 105 source

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

    Statement uses: Nat, Eq, MvPolynomial, Fin, OfNat.ofNat, Complex, P, HAdd.hAdd, Finsupp, HSub.hSub, HMul.hMul, S

    Proof uses: MvPolynomial.esymm, HPow.hPow, Neg.neg, Finset.sum, Prod, Finset.filter, LT.lt, Prod.fst, Finset.HasAntidiagonal.antidiagonal, MvPolynomial.psum, Prod.snd, MvPolynomial.mul_esymm_eq_sum, Finset, Insert.insert, Prod.mk, Singleton.singleton, LE.le, id, Eq.mpr, Finset.image and 129 more

    220 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

  13. lemma P_two_im line 132 source

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

    Statement uses: Real, Eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Real.sin, Complex.im, RingHom, MvPolynomial, Fin, Complex, Finsupp, MvPolynomial.eval, f, P

    Proof uses: Eq.mpr, Complex.exp, Complex.I, id, congrFun', congrArg, Eq.trans, MvPolynomial.X, Fin.sum_univ_three, MvPolynomial.eval_add, congr, MvPolynomial.eval_pow, MvPolynomial.eval_X, mul_pow, movire, Complex.cos, Complex.sin, Real.cos, Eq.symm, Nat.cast_zero and 70 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  14. lemma S_two_im line 140 source

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

    Statement uses: Real, Eq, HAdd.hAdd, HMul.hMul, Real.sin, OfNat.ofNat, HPow.hPow, Nat, Complex.im, RingHom, MvPolynomial, Fin, Complex, Finsupp, MvPolynomial.eval, f, S

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Complex.re, Inv.inv, HSub.hSub, Finset.sum, Finset.univ, P, MvPolynomial.C, MvPolynomial.X, HDiv.hDiv, S_two, congr, one_div, MvPolynomial.esymm_one, MvPolynomial.psum_one, map_mul and 28 more

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  15. lemma S_three_im line 145 source

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

    Statement uses: Real, Exists, Int, Eq, HAdd.hAdd, HMul.hMul, Real.pi, Complex.im, RingHom, MvPolynomial, Fin, OfNat.ofNat, Nat, Complex, Finsupp, MvPolynomial.eval, f, S

    Proof uses: Finset, Finset.powersetCard, Finset.univ, Singleton.singleton, Iff.mp, Multiset, Finset.val, Finset.val_eq_singleton_iff, rfl, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.prod, MvPolynomial.X, Finset.sum, Finset.sum_congr, Membership.mem, Eq.refl and 6 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  16. problem Usa1980P3.usa1980_p3 line 154 source

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

    Statement uses: Real, Exists, Int, Eq, HAdd.hAdd, HMul.hMul, Real.pi, Real.sin, OfNat.ofNat, HPow.hPow, Nat

    Proof uses: Eq.mpr, Complex.im, RingHom, MvPolynomial, Fin, Complex, Finsupp, MvPolynomial.eval, f, P, id, forall_congr, Nat.stepInduction, LT.lt, Nat.casesAuxOn, of_eq_true, Eq.trans, True, congrFun', congrArg and 40 more

    110 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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