Compfiles/Imo2007P6.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2007, Problem 6

Let n be a positive integer. Consider S = {(x, y, z) : x, y, z ∈ {0, 1, ... , n}, x + y + z > 0} as a set of (n + 1)³ - 1 points in three-dimensional space. Determine the smallest possible number of planes, the union of which contains S but does not include (0, 0, 0).

Imports (2)
Imported by 1 file
  1. abbrev Imo2007P6.Point line 28 source

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

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

    1 instances, coercions and auxiliary constants left out.

  2. structure Imo2007P6.Plane line 30 source

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

  3. def Imo2007P6.coordSet line 34 source

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

    Statement uses: Nat, Finset, Real

    Proof uses: Finset.map, Function.Embedding.mk, Finset.range, HAdd.hAdd, OfNat.ofNat

    6 instances, coercions and auxiliary constants left out.

  4. def Imo2007P6.S line 35 source

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

    Statement uses: Nat, Set, Imo2007P6.Point

    Proof uses: Set.ofPred, And, Fin, OfNat.ofNat, Membership.mem, Real, Finset, Imo2007P6.coordSet, GT.gt, HAdd.hAdd

    10 instances, coercions and auxiliary constants left out.

  5. def Imo2007P6.IsAdmissible line 36 source

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

    Statement uses: Nat, Finset, Imo2007P6.Plane

    Proof uses: And, Imo2007P6.Point, Membership.mem, Set, Imo2007P6.S, Exists, Eq, Real, RingHom, MvPolynomial, Fin, OfNat.ofNat, Finsupp, MvPolynomial.eval, Imo2007P6.Plane.poly, Ne

    18 instances, coercions and auxiliary constants left out.

  6. determine Imo2007P6.solution_value line 40 source

    no axioms what this means

    Statement uses: PNat, Nat

    Proof uses: HMul.hMul, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

  7. def Imo2007P6.rootFactor line 44 source

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

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

    Proof uses: HSub.hSub, Finsupp, MvPolynomial.X, RingHom, MvPolynomial.C

    22 instances, coercions and auxiliary constants left out.

  8. lemma Imo2007P6.coeff_rootFactor line 47 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Eq, Finsupp, AddMonoidAlgebra.coeff, Imo2007P6.rootFactor, Finsupp.single

    Proof uses: Eq.mpr, id, Eq.trans, ite, HSub.hSub, congrFun', congrArg, congr, MvPolynomial.X, RingHom, MvPolynomial, MvPolynomial.C, And, MvPolynomial.coeff_single_X, ite_eq_left_of_eq_true, True, eq_self, and_self, MvPolynomial.coeff_C, False.elim and 5 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  9. lemma Imo2007P6.totalDegree_rootFactor line 53 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Eq, MvPolynomial.totalDegree, Imo2007P6.rootFactor

    Proof uses: le_antisymm, id, LE.le, Eq.mp, HSub.hSub, MvPolynomial, Finsupp, MvPolynomial.X, RingHom, MvPolynomial.C, congrArg, MvPolynomial.totalDegree_X, MvPolynomial.totalDegree_sub_C_le, Membership.mem, Finset, MvPolynomial.support, Finsupp.single, of_eq_true, Eq.trans, Ne and 12 more

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  10. def Imo2007P6.rootPlane line 60 source

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

    Statement uses: Nat, Fin, OfNat.ofNat, Imo2007P6.Plane

    Proof uses: Imo2007P6.Plane.mk, Imo2007P6.rootFactor, Real, HAdd.hAdd

    8 instances, coercions and auxiliary constants left out.

  11. lemma Imo2007P6.rootFactor_inj line 64 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Eq, MvPolynomial, Imo2007P6.rootFactor, And

    Proof uses: RingHom, Finsupp, MvPolynomial.eval, congrArg, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring and 65 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  12. lemma Imo2007P6.rootPlane_injective line 76 source

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

    Statement uses: Nat, Function.Injective, Prod, Fin, OfNat.ofNat, Imo2007P6.Plane, Imo2007P6.rootPlane, Prod.fst, Prod.snd

    Proof uses: Eq, Real, HAdd.hAdd, And, Imo2007P6.rootFactor_inj, congrArg, MvPolynomial, Imo2007P6.Plane.poly, cast, Eq.refl, Nat.succ.inj, Prod.ext, Fin.ext

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  13. def Imo2007P6.examplePlanes line 82 source

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

    Statement uses: Nat, Finset, Imo2007P6.Plane

    Proof uses: Finset.map, Prod, Fin, OfNat.ofNat, Function.Embedding.mk, Imo2007P6.rootPlane, Prod.fst, Prod.snd, Imo2007P6.rootPlane_injective, Finset.univ

    3 instances, coercions and auxiliary constants left out.

  14. lemma Imo2007P6.solution_example line 85 source

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

    Statement uses: PNat, Exists, Finset, Imo2007P6.Plane, And, Imo2007P6.IsAdmissible, Eq, Nat, Finset.card, HMul.hMul, OfNat.ofNat

    Proof uses: Exists.intro, Imo2007P6.examplePlanes, And.intro, Imo2007P6.Point, Membership.mem, Set, Imo2007P6.S, Real, RingHom, MvPolynomial, Fin, Finsupp, MvPolynomial.eval, Imo2007P6.Plane.poly, Ne, LT.lt, Eq.mp, LE.le, HAdd.hAdd, congrFun' and 119 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  15. instance Imo2007P6.(instance at line 105) line 105 source
  16. lemma Imo2007P6.totalDegree_finset_prod_of_isDomain line 107 source

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

    Statement uses: DecidableEq, Finset, MvPolynomial, Fin, OfNat.ofNat, Nat, Real, Membership.mem, Ne, Finsupp, Eq, MvPolynomial.totalDegree, Finset.prod, Finset.sum

    Proof uses: Finset.induction_on, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', congrArg, MvPolynomial.totalDegree_one, eq_self, Not, Insert.insert, Finset.mem_insert_of_mem, Eq.mpr, HMul.hMul, id, Finset.prod_insert, HAdd.hAdd, Finset.sum_insert, MvPolynomial.totalDegree_mul_of_isDomain, Finset.mem_insert_self and 3 more

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  17. def Imo2007P6.planeProduct line 117 source

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

    Statement uses: Finset, Imo2007P6.Plane, MvPolynomial, Fin, OfNat.ofNat, Nat, Real

    Proof uses: Finset.prod, Finsupp, Imo2007P6.Plane.poly

    11 instances, coercions and auxiliary constants left out.

  18. lemma Imo2007P6.Plane_ne_zero line 119 source

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

    Statement uses: Imo2007P6.Plane, Ne, MvPolynomial, Fin, OfNat.ofNat, Nat, Real, Imo2007P6.Plane.poly, Finsupp

    Proof uses: id, Eq, MvPolynomial.totalDegree, Eq.mpr, congrArg, Eq.symm, Imo2007P6.Plane.totalDegree_eq_one, Eq.refl, False.elim, False, Eq.mp, Eq.trans, congrFun', MvPolynomial.totalDegree_zero

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  19. lemma Imo2007P6.planeProduct_totalDegree line 124 source

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

    Statement uses: Finset, Imo2007P6.Plane, Eq, Nat, MvPolynomial.totalDegree, Real, Fin, OfNat.ofNat, Imo2007P6.planeProduct, Finset.card

    Proof uses: Eq.mpr, Finset.prod, MvPolynomial, Finsupp, Imo2007P6.Plane.poly, id, congrArg, Imo2007P6.planeProduct.eq_1, Finset.sum, Imo2007P6.totalDegree_finset_prod_of_isDomain, Membership.mem, Imo2007P6.Plane_ne_zero, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, Finset.sum_congr, Eq.refl, Imo2007P6.Plane.totalDegree_eq_one and 3 more

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  20. lemma Imo2007P6.origin_not_mem_admissible_plane line 129 source

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

    Statement uses: Imo2007P6.Plane, Finset, PNat, Membership.mem, Imo2007P6.IsAdmissible, Ne, Real, RingHom, MvPolynomial, Fin, OfNat.ofNat, Nat, Finsupp, MvPolynomial.eval, Imo2007P6.Plane.poly

    Proof uses: And.right, Imo2007P6.Point, Set, Imo2007P6.S, Exists, And, Eq

    37 instances, coercions and auxiliary constants left out.

  21. lemma Imo2007P6.planeProduct_eval_zero_ne_zero line 132 source

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

    Statement uses: Finset, Imo2007P6.Plane, PNat, Imo2007P6.IsAdmissible, Ne, Real, RingHom, MvPolynomial, Fin, OfNat.ofNat, Nat, Finsupp, MvPolynomial.eval, Imo2007P6.planeProduct

    Proof uses: Eq.mpr, Membership.mem, Imo2007P6.Plane.poly, id, Eq, Eq.trans, Finset.prod, congrFun', congrArg, map_prod, Imo2007P6.origin_not_mem_admissible_plane

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  22. lemma Imo2007P6.planeProduct_eval_eq_zero_of_mem line 137 source

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

    Statement uses: Finset, Imo2007P6.Plane, Imo2007P6.Point, Membership.mem, Eq, Real, RingHom, MvPolynomial, Fin, OfNat.ofNat, Nat, Finsupp, MvPolynomial.eval, Imo2007P6.Plane.poly, Imo2007P6.planeProduct

    Proof uses: Eq.mpr, Finset.prod, id, congrFun', congrArg, map_prod, Finset.prod_eq_zero

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  23. def Imo2007P6.rootsInCoord line 141 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, MvPolynomial

    Proof uses: Finset.prod, Finsupp, Imo2007P6.rootFactor

    11 instances, coercions and auxiliary constants left out.

  24. def Imo2007P6.PolyFromRoots line 143 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, MvPolynomial

    Proof uses: Finset.prod, Finsupp, Finset.univ, Imo2007P6.rootsInCoord

    12 instances, coercions and auxiliary constants left out.

  25. lemma Imo2007P6.rootFactor_ne_zero line 145 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Ne, MvPolynomial, Imo2007P6.rootFactor, Finsupp

    Proof uses: Eq, False.elim, False, Eq.mp, AddMonoidAlgebra.coeff, Finsupp.single, Eq.trans, congrFun', congrArg, Imo2007P6.coeff_rootFactor

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  26. lemma Imo2007P6.totalDegree_rootsInCoord line 148 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, Eq, MvPolynomial.totalDegree, Imo2007P6.rootsInCoord, Finset.card

    Proof uses: Eq.mpr, Finset.prod, MvPolynomial, Finsupp, Imo2007P6.rootFactor, id, congrArg, Imo2007P6.rootsInCoord.eq_1, Finset.sum, Imo2007P6.totalDegree_finset_prod_of_isDomain, Membership.mem, Imo2007P6.rootFactor_ne_zero, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, Finset.sum_congr, Eq.refl, Imo2007P6.totalDegree_rootFactor and 3 more

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  27. lemma Imo2007P6.rootsInCoord_ne_zero line 154 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, Ne, MvPolynomial, Imo2007P6.rootsInCoord, Finsupp

    Proof uses: Iff.mpr, Finset.prod, Imo2007P6.rootFactor, Membership.mem, Finset.prod_ne_zero_iff, Imo2007P6.rootFactor_ne_zero

    34 instances, coercions and auxiliary constants left out.

  28. lemma Imo2007P6.totalDegree_PolyFromRoots line 157 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, MvPolynomial, Eq, Imo2007P6.PolyFromRoots, MvPolynomial.totalDegree, Finset.sum, Finset.univ, Finset.card

    Proof uses: Eq.mpr, id, congrArg, Finset.prod, Finsupp, Imo2007P6.rootsInCoord, Imo2007P6.PolyFromRoots.eq_1, Imo2007P6.totalDegree_finset_prod_of_isDomain, Membership.mem, Imo2007P6.rootsInCoord_ne_zero, of_eq_true, Eq.trans, True, congrFun', Finset.sum_congr, Eq.refl, Imo2007P6.totalDegree_rootsInCoord, eq_self

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  29. lemma Imo2007P6.coeff_rootFactor_mul_top line 163 source

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

    Statement uses: MvPolynomial, Fin, OfNat.ofNat, Nat, Real, Finsupp, Eq, MvPolynomial.totalDegree, AddMonoidHom, Finsupp.degree, AddMonoidAlgebra.coeff, HMul.hMul, Imo2007P6.rootFactor, HAdd.hAdd, Finsupp.single

    Proof uses: RingHom, MvPolynomial.C, Eq.mpr, id, congrArg, MvPolynomial.coeff_C_mul, MvPolynomial.coeff_eq_zero_of_totalDegree_lt, LT.lt, Finset.sum, Finsupp.support, Eq.symm, Finsupp.degree_apply, map_add, Finsupp.degree_single, MulZeroClass.mul_zero, Eq.refl, of_eq_true, Eq.trans, True, congrFun' and 19 more

    108 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  30. lemma Imo2007P6.coeff_rootFactorFinset_mul_top line 172 source

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

    Statement uses: Finset, Real, Fin, OfNat.ofNat, Nat, MvPolynomial, Finsupp, Eq, MvPolynomial.totalDegree, AddMonoidHom, Finsupp.degree, AddMonoidAlgebra.coeff, HMul.hMul, Finset.prod, Imo2007P6.rootFactor, HAdd.hAdd, Finsupp.single, Finset.card

    Proof uses: Finset.induction_on, of_eq_true, EmptyCollection.emptyCollection, Eq.trans, True, congrFun', congrArg, congr, one_mul, Finsupp.single_zero, add_zero, eq_self, Not, Membership.mem, Ne, False.elim, False, Eq.mp, Iff.mpr, Finset.prod_ne_zero_iff and 28 more

    111 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  31. lemma Imo2007P6.coeff_rootsInCoordFinset_top line 193 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, Eq, Finsupp, AddMonoidAlgebra.coeff, Finset.prod, MvPolynomial, Imo2007P6.rootsInCoord, Finset.sum, Finsupp.single, Finset.card

    Proof uses: Finset.induction_on, of_eq_true, EmptyCollection.emptyCollection, Eq.trans, True, congrFun', congrArg, AddMonoidAlgebra.coeff_one_zero, eq_self, Not, Membership.mem, MvPolynomial.totalDegree, AddMonoidHom, Finsupp.degree, Eq.mpr, id, Imo2007P6.totalDegree_finset_prod_of_isDomain, Imo2007P6.rootsInCoord_ne_zero, congr, Finset.sum_congr and 18 more

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  32. lemma Imo2007P6.coeff_card line 206 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, MvPolynomial, Finsupp, Eq, Imo2007P6.PolyFromRoots, Finset.card, AddMonoidAlgebra.coeff

    Proof uses: Eq.mpr, id, congrArg, Finset.prod, Finset.univ, Imo2007P6.rootsInCoord, Imo2007P6.PolyFromRoots.eq_1, Finset.sum, Finsupp.single, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, Finsupp.ext, List, List.Mem, List.finRange and 32 more

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  33. lemma Imo2007P6.eval_rootsInCoord_eq_zero line 214 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, Imo2007P6.Point, Membership.mem, Eq, RingHom, MvPolynomial, Finsupp, MvPolynomial.eval, Imo2007P6.rootsInCoord

    Proof uses: Eq.mpr, Finset.prod, Imo2007P6.rootFactor, id, congrFun', congrArg, map_prod, Finset.prod_eq_zero, of_eq_true, Eq.trans, True, HSub.hSub, MvPolynomial.X, MvPolynomial.C, map_sub, congr, MvPolynomial.eval_X, MvPolynomial.eval_C, sub_self, eq_self

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  34. lemma Imo2007P6.zeros line 218 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Finset, Real, MvPolynomial, Eq, Imo2007P6.PolyFromRoots, Exists, Membership.mem, RingHom, Finsupp, MvPolynomial.eval

    Proof uses: Eq.mpr, Finset.prod, Finset.univ, Imo2007P6.rootsInCoord, id, congrFun', congrArg, Eq.trans, map_prod, Finset.prod_eq_zero, Finset.mem_univ, Imo2007P6.eval_rootsInCoord_eq_zero

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  35. def Imo2007P6.positiveCoordSet line 225 source

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

    Statement uses: Nat, Finset, Real

    Proof uses: Finset.map, Function.Embedding.mk, Finset.Icc, OfNat.ofNat

    6 instances, coercions and auxiliary constants left out.

  36. lemma Imo2007P6.mem_S_of_mem_coordSet_of_ne_zero line 227 source

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

    Statement uses: Nat, Imo2007P6.Point, Fin, OfNat.ofNat, Membership.mem, Real, Finset, Imo2007P6.coordSet, Ne, Set, Imo2007P6.S

    Proof uses: And.intro, GT.gt, HAdd.hAdd, Exists, Iff.mp, Function.ne_iff, LE.le, And, Eq, Eq.mp, forall_congr, Finset.map, Function.Embedding.mk, Finset.range, Eq.trans, Function.Embedding, congrArg, funext, congrFun', LT.lt and 29 more

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  37. lemma Imo2007P6.exists_poly_of_IsAdmissible line 239 source

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

    Statement uses: PNat, Finset, Imo2007P6.Plane, Imo2007P6.IsAdmissible, Exists, MvPolynomial, Fin, OfNat.ofNat, Nat, Real, And, Eq, MvPolynomial.totalDegree, Finset.card, Ne, RingHom, Finsupp, MvPolynomial.eval, Imo2007P6.Point, Membership.mem and 2 more

    Proof uses: Exists.intro, Imo2007P6.planeProduct, And.intro, Imo2007P6.planeProduct_totalDegree, Imo2007P6.planeProduct_eval_zero_ne_zero, Imo2007P6.Plane.poly, And.left, Imo2007P6.planeProduct_eval_eq_zero_of_mem

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  38. lemma Imo2007P6.min_total_degree line 246 source

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

    Statement uses: Nat, MvPolynomial, Fin, OfNat.ofNat, Real, Ne, RingHom, Finsupp, MvPolynomial.eval, Imo2007P6.Point, Membership.mem, Set, Imo2007P6.S, Eq, LE.le, HMul.hMul, MvPolynomial.totalDegree

    Proof uses: Decidable.byContradiction, Not, Finset, Imo2007P6.positiveCoordSet, Imo2007P6.PolyFromRoots, HDiv.hDiv, HSub.hSub, HSMul.hSMul, Equiv, Equiv.symm, Finsupp.equivFunOnFinite, Matrix.vecCons, Matrix.vecEmpty, AddMonoidHom, Finsupp.degree, Nat.succ, List, List.Mem, List.finRange, HEq and 88 more

    180 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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

  39. lemma Imo2007P6.solution_lowerBounds line 312 source

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

    Statement uses: PNat, Membership.mem, Nat, Set, lowerBounds, Set.ofPred, Exists, Finset, Imo2007P6.Plane, And, Imo2007P6.IsAdmissible, Eq, Finset.card, Imo2007P6.solution_value

    Proof uses: Eq.mpr, LE.le, HMul.hMul, OfNat.ofNat, id, Eq.trans, forall_congr, MvPolynomial, Fin, Real, MvPolynomial.totalDegree, Ne, RingHom, Finsupp, MvPolynomial.eval, Imo2007P6.Point, Imo2007P6.S, Imo2007P6.exists_poly_of_IsAdmissible, congrArg, Eq.symm and 1 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  40. problem Imo2007P6.imo2007_p6 line 322 source

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

    Statement uses: PNat, IsLeast, Nat, Set.ofPred, Exists, Finset, Imo2007P6.Plane, And, Imo2007P6.IsAdmissible, Eq, Finset.card, Imo2007P6.solution_value

    Proof uses: And.intro, Membership.mem, Set, lowerBounds, Imo2007P6.solution_example, Imo2007P6.solution_lowerBounds

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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