FormalConjecturesForMathlib/Data/Nat/Init.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Nat.dvd_add_mul_self line 25 source

   standard axioms: propext what this means

   Statement uses: Nat, Iff, Dvd.dvd, HAdd.hAdd, HMul.hMul

   Proof uses: Eq.mpr, id, Eq, congrArg, propext, Nat.dvd_add_left, Nat.dvd_mul_left, Iff.rfl

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

2. lemma Nat.dvd_add_self_mul line 28 source

   standard axioms: propext what this means

   Statement uses: Nat, Iff, Dvd.dvd, HAdd.hAdd, HMul.hMul

   Proof uses: Eq.mpr, id, Eq, congrArg, Nat.mul_comm, propext, Nat.dvd_add_mul_self, Iff.rfl

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

3. lemma Nat.dvd_mul_self_add line 31 source

   standard axioms: propext what this means

   Statement uses: Nat, Iff, Dvd.dvd, HAdd.hAdd, HMul.hMul

   Proof uses: Eq.mpr, id, Eq, congrArg, Nat.add_comm, propext, Nat.dvd_add_mul_self, Iff.rfl

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

4. lemma Nat.dvd_self_mul_add line 34 source

   standard axioms: propext what this means

   Statement uses: Nat, Iff, Dvd.dvd, HAdd.hAdd, HMul.hMul

   Proof uses: Eq.mpr, id, Eq, congrArg, Nat.mul_comm, propext, Nat.dvd_mul_self_add, Iff.rfl

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

5. lemma Nat.dvd_sub_iff_right' line 37 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Dvd.dvd, Iff, HSub.hSub, Or, LE.le

   Proof uses: Nat.le_total, of_eq_true, Eq.trans, True, congr, congrArg, OfNat.ofNat, Nat.sub_eq_zero_of_le, eq_true, or_true, iff_self, congrFun', implies_congr_ctx, Eq.refl, Nat.le_antisymm, implies_true

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

6. lemma Nat.dvd_sub_iff_left' line 42 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Dvd.dvd, Iff, HSub.hSub, Or, LE.le

   Proof uses: Nat.le_total, of_eq_true, Eq.trans, True, congr, congrArg, OfNat.ofNat, Nat.sub_eq_zero_of_le, eq_true, or_true, iff_self, congrFun', implies_congr_ctx, Eq.refl, Eq.symm, Nat.le_antisymm, implies_true

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

7. lemma Nat.dvd_sub_mul_self line 47 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Iff, Dvd.dvd, HSub.hSub, HMul.hMul, Or, LE.le

   Proof uses: Eq.mpr, id, Eq, congrArg, propext, Nat.dvd_sub_iff_left', Nat.dvd_mul_left, Iff.rfl

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

8. lemma Nat.dvd_sub_self_mul line 50 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Iff, Dvd.dvd, HSub.hSub, HMul.hMul, Or, LE.le

   Proof uses: Eq.mpr, id, Eq, congrArg, Nat.mul_comm, propext, Nat.dvd_sub_mul_self, Iff.rfl

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

9. lemma Nat.dvd_mul_self_sub line 53 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Iff, Dvd.dvd, HSub.hSub, HMul.hMul, Or, LE.le

   Proof uses: Eq.mpr, id, Eq, congrArg, propext, Nat.dvd_sub_iff_right', Nat.dvd_mul_left, Iff.rfl

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

10. lemma Nat.dvd_self_mul_sub line 56 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat, Iff, Dvd.dvd, HSub.hSub, HMul.hMul, Or, LE.le

    Proof uses: Eq.mpr, id, Eq, congrArg, Nat.mul_comm, propext, Nat.dvd_mul_self_sub, Iff.rfl

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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