Compfiles/Imo1975P5.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. determine Imo1975P5.constructible line 26 source

   no axioms what this means

   Statement uses: Bool

   Proof uses: Bool.true

2. theorem Imo1975P5.not_irrational_add line 30 source

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

   Statement uses: Real, Not, Irrational, HAdd.hAdd

   Proof uses: Iff.mpr, Or, not_imp_not, Irrational.add_cases, not_or_intro

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

3. theorem Imo1975P5.not_irrational_sub line 35 source

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

   Statement uses: Real, Not, Irrational, HSub.hSub

   Proof uses: Iff.mpr, Or, Neg.neg, HAdd.hAdd, not_imp_not, Irrational.add_cases, not_or_intro, Eq.mpr, id, Eq, congrArg, propext, irrational_neg_iff

   5 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

4. theorem Imo1975P5.not_irrational_mul line 42 source

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

   Statement uses: Real, Not, Irrational, HMul.hMul

   Proof uses: Iff.mpr, Or, not_imp_not, Irrational.mul_cases, not_or_intro

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

5. theorem Imo1975P5.irrational_abs_iff line 47 source

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

   Statement uses: Real, Iff, Irrational, abs

   Proof uses: abs_by_cases, Iff.rfl, irrational_neg_iff

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

6. def Imo1975P5.θ line 52 source

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

   Statement uses: Real

   Proof uses: Real.arccos, HDiv.hDiv, OfNat.ofNat

   7 instances, coercions and auxiliary constants left out.

7. theorem Imo1975P5.sin_θ line 54 source

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

   Statement uses: Eq, Real, Real.sin, Imo1975P5.θ, HDiv.hDiv, Rat, OfNat.ofNat

   Proof uses: id, Eq.mpr, Real.arccos, Real.sqrt, HSub.hSub, HPow.hPow, Nat, congrArg, Real.sin_arccos, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, NNRat.rawCast, Mathlib.Tactic.Ring.cast_nnrat, Mathlib.Meta.NormNum.isNNRat_realSqrt_of_isNNRat, Eq.refl, Mathlib.Meta.NormNum.IsRat.to_isNNRat, Mathlib.Meta.NormNum.isRat_sub, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.IsNat.to_isNNRat and 16 more

   66 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

8. theorem Imo1975P5.cos_θ line 59 source

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

   Statement uses: Eq, Real, Real.cos, Imo1975P5.θ, HDiv.hDiv, Rat, OfNat.ofNat

   Proof uses: id, Eq.mpr, Real.arccos, congrArg, Real.cos_arccos, le_of_not_gt, Neg.neg, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Nat, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Ring and 65 more

   104 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

9. def Imo1975P5.P line 64 source

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

   Statement uses: Nat, Circle

   Proof uses: ContinuousMap, Real, Circle.exp, HMul.hMul, Imo1975P5.θ, OfNat.ofNat

   12 instances, coercions and auxiliary constants left out.

10. lemma Imo1975P5.P_cast_eq line 66 source

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

    Statement uses: Nat, Eq, Complex, Membership.mem, Submonoid, Submonoid.unitSphere, Imo1975P5.P, Complex.mk, Real.cos, HMul.hMul, Real, Imo1975P5.θ, OfNat.ofNat, Real.sin

    Proof uses: Eq.mpr, ContinuousMap, Circle, Circle.exp, id, congrArg, Imo1975P5.P.eq_1, Complex.exp, Complex.I, Circle.coe_exp, And, Complex.re, Complex.im, propext, Complex.ext_iff, congr, congrFun', Eq.trans, Real.exp, Complex.ofReal_mul and 41 more

    93 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

11. theorem Imo1975P5.not_irrational_sin_θ_mul_and_not_irrational_cos_θ_mul line 72 source

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

    Statement uses: Nat, And, Not, Irrational, Real.sin, HMul.hMul, Real, Imo1975P5.θ, Real.cos

    Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, False, CharP.cast_eq_zero, MulZeroClass.mul_zero, Real.sin_zero, not_false_eq_true, Real.cos_zero, and_self, Eq.mpr, HAdd.hAdd, id, Eq, Nat.cast_add, mul_add and 3 more

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

12. lemma Imo1975P5.Circle.dist_eq line 80 source

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

    Statement uses: Circle, Eq, Real, Dist.dist, Complex, Membership.mem, Submonoid, Submonoid.unitSphere

    Proof uses: rfl

    22 instances, coercions and auxiliary constants left out.

13. theorem Imo1975P5.not_irrational_dist_P_P line 82 source

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

    Statement uses: Nat, Not, Irrational, Dist.dist, Circle, Imo1975P5.P

    Proof uses: id, Eq.mpr, Complex, Membership.mem, Submonoid, Submonoid.unitSphere, Complex.mk, Real.cos, HMul.hMul, Real, Imo1975P5.θ, OfNat.ofNat, Real.sin, Eq, congrArg, congr, Imo1975P5.P_cast_eq, Real.sqrt, HAdd.hAdd, HPow.hPow and 33 more

    113 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

14. theorem Imo1975P5.sin_mul_θ_ne_zero line 96 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Ne, Real, Real.sin, HMul.hMul, Imo1975P5.θ

    Proof uses: id, Eq, Membership.mem, Set, Insert.insert, Neg.neg, HDiv.hDiv, Singleton.singleton, niven_sin, Exists, Int, Real.pi, Rat, Eq.mp, congrArg, propext, Real.sin_eq_zero_iff, Exists.intro, Eq.mpr, congrFun' and 17 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

15. theorem Imo1975P5.P_injective line 114 source

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

    Statement uses: Function.Injective, Nat, Circle, Imo1975P5.P

    Proof uses: Eq, Mathlib.Tactic.Contrapose.contrapose₁, id, Not, Ne, LT.lt, Or, Classical.em, Eq.mpr, Complex, Membership.mem, Submonoid, Submonoid.unitSphere, congrArg, Complex.mk, Real.cos, HMul.hMul, Real, Imo1975P5.θ, OfNat.ofNat and 15 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

16. problem Imo1975P5.imo1975_p5 line 134 source

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

    Statement uses: Iff, Eq, Bool, Imo1975P5.constructible, Bool.true, Exists, Finset, Circle, And, Nat, Finset.card, OfNat.ofNat, Set.Pairwise, Not, Irrational, Dist.dist

    Proof uses: Eq.mpr, id, Eq.trans, True, congrFun', congrArg, eq_self, true_iff, Exists.intro, Finset.map, Function.Embedding.mk, Imo1975P5.P, Imo1975P5.P_injective, Finset.range, And.intro, of_eq_true, Finset.card_map, Finset.card_range, Membership.mem, Set and 11 more

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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