Compfiles/Usa1998P3.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1998, Problem 3

Let a₀,a₁,...,aₙ be real numbers from the interval (0,π/2) such that

tan(a₀ - π/4) + tan(a₁ - π/4) + ... + tan(aₙ - π/4) ≥ n - 1.

Prove that

tan(a₀)tan(a₁)...tan(aₙ) ≥ nⁿ⁺¹.

Imports (5)
Imported by 1 file
  1. lemma Usa1998P3.lemma0 line 37 source

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

    Statement uses: LE.le, Set, Real, Set.Icc, HDiv.hDiv, Neg.neg, Real.pi, OfNat.ofNat, Nat, Set.Ioo

    Proof uses: Membership.mem, And.intro, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring, Int.rawCast and 69 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  2. lemma Usa1998P3.lemma1 line 42 source

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

    Statement uses: Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, HDiv.hDiv, Real.pi, Nat, LT.lt, Real.tan, HSub.hSub

    Proof uses: Eq, id, Eq.mpr, Inv.inv, congrArg, Real.tan_pi_div_two_sub, Real.tan_pi_div_four, propext, one_eq_inv, Eq.refl, Eq.symm, StrictMonoOn, Set.Icc, sub_lt_sub_right, HAdd.hAdd, StrictMonoOn.comp, Neg.neg, StrictMonoOn.mono, Real.strictMonoOn_tan, Usa1998P3.lemma0 and 82 more

    124 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

  3. lemma Usa1998P3.lemma2' line 73 source

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

    Statement uses: Nat, Eq, Finset, Finset.erase, Finset.range, HAdd.hAdd, OfNat.ofNat

    Proof uses: Eq.mpr, Nat.succ, id, congrArg, Eq.symm, Nat.succ_eq_add_one, Insert.insert, Finset.range_add_one, of_eq_true, Eq.trans, True, congrFun', Finset.erase_insert_eq_erase, Finset.erase_eq_of_notMem, Not, Membership.mem, False, LT.lt, not_false_eq_true, eq_self

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. lemma Usa1998P3.lemma2 line 76 source

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

    Statement uses: Nat, Real, Eq, Finset.prod, Finset.range, HAdd.hAdd, OfNat.ofNat, Finset.erase, HPow.hPow

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Singleton.singleton, Finset, EmptyCollection.emptyCollection, zero_add, funext, Finset.prod_congr, congrFun', Membership.mem, Eq.refl, Finset.prod_singleton, Finset.erase_singleton, CharP.cast_eq_zero, Real.rpow_zero, Finset.prod_const_one and 48 more

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 40 steps

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

  5. problem Usa1998P3.usa1998_p3 line 131 source

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

    Statement uses: Nat, Real, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Set, Set.Ioo, HDiv.hDiv, Real.pi, LE.le, HSub.hSub, Finset.sum, Real.tan, HPow.hPow, Finset.prod

    Proof uses: Eq, Ne, Or, eq_or_ne, Eq.mpr, id, congr, congrArg, Eq.trans, CharP.cast_eq_zero, congrFun', zero_add, pow_one, Singleton.singleton, Finset.prod_singleton, Real.tan_nonneg_of_nonneg_of_le_pi_div_two, le_of_lt, And.left, LT.lt, Eq.mp and 211 more

    246 instances, coercions and auxiliary constants left out.

    Tactic trace: 138 steps

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