Compfiles/Imo2024P1.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def Imo2024P1.Condition line 36 source

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

   Statement uses: Real

   Proof uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, Int, Finset.sum, Finset.Icc, Int.floor, HMul.hMul

   14 instances, coercions and auxiliary constants left out.

2. lemma Imo2024P1.condition_two_mul_int line 38 source

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

   Statement uses: Int, Imo2024P1.Condition, HMul.hMul, Real, OfNat.ofNat, Nat

   Proof uses: LT.lt, Dvd.dvd, Finset.sum, Finset.Icc, Int.floor, Eq.mpr, id, Eq, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Int.floor_intCast, Finset.Ico, Order.succ, congrFun', Finset.range, dvd_mul_of_dvd_left, Eq.symm and 31 more

   116 instances, coercions and auxiliary constants left out.

   Tactic trace: 9 steps

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

3. lemma Imo2024P1.condition_sub_two_mul_int_iff line 49 source

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

   Statement uses: Real, Int, Iff, Imo2024P1.Condition, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat

   Proof uses: id, forall_congr', LT.lt, Dvd.dvd, Finset.sum, Finset.Icc, Int.floor, imp_congr_right, dvd_iff_dvd_of_dvd_sub, Eq.mpr, Eq, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, congrFun', mul_sub, Eq.trans, Eq.symm and 15 more

   80 instances, coercions and auxiliary constants left out.

   Tactic trace: 10 steps

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

4. lemma Imo2024P1.condition_toIcoMod_iff line 61 source

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

   Statement uses: Real, Iff, Imo2024P1.Condition, toIcoMod, OfNat.ofNat, Nat

   Proof uses: Eq.mpr, HSub.hSub, HSMul.hSMul, Int, toIcoDiv, id, Eq, congrArg, toIcoMod.eq_1, HMul.hMul, zsmul_eq_mul, mul_comm, propext, Imo2024P1.condition_sub_two_mul_int_iff, Iff.rfl

   52 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

5. lemma Imo2024P1.Condition.mem_Ico_one_of_mem_Ioo line 71 source

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

   Statement uses: Real, Imo2024P1.Condition, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Nat, Set.Ico

   Proof uses: LT.lt, And.intro, LE.le, Decidable.byContradiction, Not, Nat.ceil, Inv.inv, Eq.mpr, id, Eq, congrArg, propext, Nat.lt_ceil, cast, Eq.trans, congrFun', Eq.symm, Nat.cast_one, Iff.mpr, one_lt_inv₀ and 98 more

   140 instances, coercions and auxiliary constants left out.

   Tactic trace: 40 steps

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

6. lemma Imo2024P1.Condition.mem_Ico_n_of_mem_Ioo line 102 source

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

   Statement uses: Real, Imo2024P1.Condition, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Nat, LT.lt, Set.Ico, HDiv.hDiv, HSub.hSub, HMul.hMul

   Proof uses: And, Eq, Int, Finset.sum, Finset.Icc, Int.floor, HPow.hPow, Nat.le_induction, Nat.succ, LE.le, Imo2024P1.Condition.mem_Ico_one_of_mem_Ioo, Eq.mpr, HAdd.hAdd, id, congr, congrArg, Eq.trans, Singleton.singleton, Finset, Finset.sum_congr and 170 more

   226 instances, coercions and auxiliary constants left out.

   Tactic trace: 58 steps

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

7. lemma Imo2024P1.not_condition_of_mem_Ioo line 155 source

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

   Statement uses: Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Nat, Not, Imo2024P1.Condition

   Proof uses: HAdd.hAdd, Nat.floor, Inv.inv, HSub.hSub, LT.lt, LE.le, HDiv.hDiv, HMul.hMul, And.left, Imo2024P1.Condition.mem_Ico_n_of_mem_Ioo, False, Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true and 96 more

   142 instances, coercions and auxiliary constants left out.

   Tactic trace: 14 steps

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

8. lemma Imo2024P1.condition_iff_of_mem_Ico line 169 source

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

   Statement uses: Real, Membership.mem, Set, Set.Ico, OfNat.ofNat, Nat, Iff, Imo2024P1.Condition, Eq

   Proof uses: Iff.intro, Set.Ioo, Or, Set.eq_left_or_mem_Ioo_of_mem_Ico, Eq.refl, Eq.symm, False.elim, Imo2024P1.not_condition_of_mem_Ioo, Eq.mpr, HMul.hMul, Int, eq_of_heq, HEq, HEq.refl, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_intCast and 1 more

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 12 steps

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

9. determine Imo2024P1.solutionSet line 181 source

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

   Statement uses: Set, Real

   Proof uses: Set.ofPred, Exists, Int, Eq, HMul.hMul, OfNat.ofNat

   7 instances, coercions and auxiliary constants left out.

10. problem Imo2024P1.imo2024_p1 line 183 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo2024P1.solutionSet, Nat, LT.lt, OfNat.ofNat, Dvd.dvd, Int, Finset.sum, Finset.Icc, Int.floor, HMul.hMul

    Proof uses: Iff.intro, Eq, Imo2024P1.condition_two_mul_int, Eq.symm, id, Imo2024P1.Condition, HSMul.hSMul, Exists, Eq.mp, HSub.hSub, congrArg, funext, congrFun', sub_zero, AddCommGroup.ModEq, propext, AddCommGroup.modEq_iff_zsmul', toIcoMod, AddCommGroup.modEq_iff_toIcoMod_eq_left, Imo2024P1.condition_iff_of_mem_Ico and 12 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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