Compfiles/Imo1971P5.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1971, Problem 5

Prove that for every natural number m there exists a nonempty finite set S of points in the plane with the following property: For every point s in S, there are exactly m points which are at a unit distance from s.

Imports (2)
Imported by 1 file
  1. abbrev Imo1971P5.Pt line 30 source

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

    Proof uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

  2. lemma Imo1971P5.norm_one_infinity line 34 source

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

    Statement uses: Set.Infinite, Imo1971P5.Pt, Set.ofPred, Eq, Real, Norm.norm, OfNat.ofNat, ENNReal, Fin, Nat

    Proof uses: Metric.sphere, IsPreconnected.infinite_of_nontrivial, isPreconnected_sphere, Eq.mpr, LT.lt, Cardinal, Module.rank, Module.finrank, id, congrArg, Eq.symm, Module.finrank_eq_rank, EuclideanSpace, finrank_euclideanSpace_fin, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.isNat_natCast, Eq.refl, Bool and 34 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  3. lemma Imo1971P5.exists_three_of_infinite line 50 source

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

    Statement uses: Set, Set.Infinite, Exists, And, Membership.mem, Ne

    Proof uses: Set.Nontrivial, Set.Infinite.nontrivial, SDiff.sdiff, Insert.insert, Singleton.singleton, Set.Nonempty, Set.Infinite.nonempty, Set.Infinite.sdiff, Set.toFinite, Not, Exists.intro, And.intro, Eq, And.right, Eq.mp, Eq.trans, Or, congrArg, Eq.symm, And.left

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  4. lemma Imo1971P5.sphere_inter_finite line 59 source

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

    Statement uses: EuclideanGeometry.Sphere, Imo1971P5.Pt, OfNat.ofNat, ENNReal, Fin, Nat, Real, Ne, Set.Finite, Inter.inter, Set, Metric.sphere, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.radius

    Proof uses: Classical.byContradiction, Not, Exists, And, Membership.mem, False, Imo1971P5.exists_three_of_infinite, Eq.mp, Set.Infinite, Eq, Module.finrank, EuclideanSpace, finrank_euclideanSpace_fin, Or, EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two, And.left, congrArg, propext, EuclideanGeometry.Sphere.mem_coe, Set.mem_inter_iff and 1 more

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  5. lemma Imo1971P5.sphere_eq_sub_norm line 70 source

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

    Statement uses: Imo1971P5.Pt, Real, Eq, Set, Set.ofPred, Norm.norm, OfNat.ofNat, ENNReal, Fin, Nat, HSub.hSub, Metric.sphere, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.mk, EuclideanGeometry.Sphere.radius

    Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, id, congrArg, Set.mem_ofPred_eq, propext, mem_sphere_iff_norm, Iff.rfl

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. lemma Imo1971P5.norm_one_inter_finite line 75 source

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

    Statement uses: Imo1971P5.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, Set.Finite, Inter.inter, Set, Set.ofPred, Eq, Norm.norm, HSub.hSub

    Proof uses: Eq.mpr, Metric.sphere, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.mk, EuclideanGeometry.Sphere.radius, id, congrArg, Imo1971P5.sphere_eq_sub_norm, Imo1971P5.sphere_inter_finite, EuclideanGeometry.Sphere, Not, ne_eq, And, propext, EuclideanGeometry.Sphere.ext_iff, and_iff_left, rfl, Eq.symm, Ne.symm

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  7. lemma Imo1971P5.finite₁ line 85 source

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

    Statement uses: Set, Imo1971P5.Pt, Set.Finite, Set.ofPred, Exists, And, Membership.mem, Eq, HSub.hSub, OfNat.ofNat, ENNReal, Fin, Nat, Real

    Proof uses: Set.iUnion, Singleton.singleton, Set.ext, Eq.mpr, Iff, id, congr, congrArg, congrFun', funext, Eq.trans, propext, exists_prop_congr, Iff.of_eq, Eq.refl, Iff.intro, Exists.intro, and_iff_right, Set.Finite.biUnion, Set.finite_singleton

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  8. lemma Imo1971P5.finite₂ line 100 source

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

    Statement uses: Set, Imo1971P5.Pt, Set.Finite, Set.ofPred, Exists, And, Membership.mem, Ne, Eq, Real, Norm.norm, OfNat.ofNat, ENNReal, Fin, Nat, Dist.dist, HAdd.hAdd

    Proof uses: Set.iUnion, Set.ext, Eq.mpr, Iff, Not, id, congr, congrArg, congrFun', funext, Eq.trans, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, propext, exists_prop_congr, Iff.intro, Exists.intro, and_iff_right, And.intro and 44 more

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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

  9. problem Imo1971P5.imo1971_p5 line 135 source

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

    Statement uses: Nat, Exists, Set, Imo1971P5.Pt, And, Set.Nonempty, Set.Finite, Membership.mem, Eq, ENat, Set.encard, Set.ofPred, Real, Dist.dist, OfNat.ofNat, ENNReal, Fin

    Proof uses: Nat.recAux, Exists.intro, Singleton.singleton, And.intro, Set.singleton_nonempty, Set.finite_singleton, Eq.mpr, id, congrArg, Nat.cast_zero, EmptyCollection.emptyCollection, propext, Set.encard_eq_zero, Not, Set.eq_empty_iff_forall_notMem, False, False.elim, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_eq_false and 72 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 125 steps

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