Compfiles/Usa1996P6.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def Usa1996P6.UniqueRepresentationSet line 29 source

   no axioms what this means

   Statement uses: Set, Int

   Proof uses: ExistsUnique, Prod, And, Membership.mem, Prod.fst, Prod.snd, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat

   6 instances, coercions and auxiliary constants left out.

2. def Usa1996P6.negFourValue line 35 source

   standard axioms: propext what this means

   Statement uses: Nat, List, Fin, Int

   Proof uses: Nat.ofDigits, Neg.neg, OfNat.ofNat, List.map

   4 instances, coercions and auxiliary constants left out.

3. lemma Usa1996P6.negFourValue_nil line 39 source

   standard axioms: propext what this means

   Statement uses: Nat, Eq, Int, Usa1996P6.negFourValue, List.nil, Fin, OfNat.ofNat

   Proof uses: rfl

   1 instances, coercions and auxiliary constants left out.

4. lemma Usa1996P6.negFourValue_cons line 42 source

   standard axioms: propext what this means

   Statement uses: Nat, Fin, List, Eq, Int, Usa1996P6.negFourValue, List.cons, HAdd.hAdd, HMul.hMul, Neg.neg, OfNat.ofNat

   Proof uses: rfl

   9 instances, coercions and auxiliary constants left out.

5. def Usa1996P6.lowBit line 45 source

   standard axioms: propext what this means

   Statement uses: Fin, OfNat.ofNat, Nat

   Proof uses: Usa1996P6.lowBit.match_1, Unit

   5 instances, coercions and auxiliary constants left out.

6. def Usa1996P6.highBit line 52 source

   standard axioms: propext what this means

   Statement uses: Fin, OfNat.ofNat, Nat

   Proof uses: Usa1996P6.highBit.match_1, Unit

   5 instances, coercions and auxiliary constants left out.

7. lemma Usa1996P6.lowBit_add_two_mul_highBit line 58 source

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

   Statement uses: Fin, OfNat.ofNat, Nat, Eq, Int, HAdd.hAdd, Usa1996P6.lowBit, HMul.hMul, Usa1996P6.highBit

   Proof uses: LT.lt, Or, Fin.mk, Eq.refl, Eq.symm

   23 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

8. lemma Usa1996P6.negFourQuotient_natAbs_lt line 64 source

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

   Statement uses: Int, Ne, OfNat.ofNat, Neg.neg, LT.lt, Nat, Int.natAbs, HDiv.hDiv

   Proof uses: LE.le, HMod.hMod, Int.emod_nonneg, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl, Int.emod_lt_abs, HAdd.hAdd, HMul.hMul, Int.emod_add_mul_ediv, dite, Int.ofNat_natAbs_of_nonpos, Int.natAbs_of_nonneg, Iff.mp, Int.ofNat_lt, Not and 5 more

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 28 steps

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

9. lemma Usa1996P6.exists_negFourExpansion line 86 source

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

   Statement uses: Int, Exists, List, Fin, OfNat.ofNat, Nat, Eq, Usa1996P6.negFourValue

   Proof uses: WellFounded.induction, WellFoundedRelation.rel, measure, Int.natAbs, WellFoundedRelation.wf, dite, Exists.intro, List.nil, rfl, Eq.symm, Not, Neg.neg, List.cons, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.ofDigits, List.map and 35 more

   45 instances, coercions and auxiliary constants left out.

   Tactic trace: 25 steps

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

10. lemma Usa1996P6.negFourValue_split line 108 source

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

    Statement uses: List, Fin, OfNat.ofNat, Nat, Eq, Int, Usa1996P6.negFourValue, HAdd.hAdd, List.map, Usa1996P6.lowBit, HMul.hMul, Usa1996P6.highBit

    Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrArg, congr, List.map_nil, MulZeroClass.mul_zero, add_zero, eq_self, Eq.mpr, List.cons, Neg.neg, id, List.map_cons, Usa1996P6.lowBit_add_two_mul_highBit, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 33 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

11. def Usa1996P6.headBit line 118 source

    standard axioms: propext what this means

    Statement uses: List, Fin, OfNat.ofNat, Nat

    Proof uses: Usa1996P6.headBit.match_1, Unit

    4 instances, coercions and auxiliary constants left out.

12. lemma Usa1996P6.negFourValue_eq_headBit_add_tail line 122 source

    standard axioms: propext what this means

    Statement uses: List, Fin, OfNat.ofNat, Nat, Eq, Int, Usa1996P6.negFourValue, HAdd.hAdd, Usa1996P6.headBit, HMul.hMul, Neg.neg, List.tail

    Proof uses: List.nil, Eq.refl, Eq.symm, List.cons

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

13. lemma Usa1996P6.binary_pair_unique_aux line 126 source

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

    Statement uses: Nat, List, Fin, OfNat.ofNat, LE.le, HAdd.hAdd, List.length, Eq, Int, Usa1996P6.negFourValue, HMul.hMul, And

    Proof uses: Nat.recAux, List.nil, Iff.mp, List.length_eq_zero_iff, of_eq_true, Eq.trans, True, congr, congrArg, eq_self, and_self, Eq.symm, List.tail, Eq.mpr, HSub.hSub, id, congrFun', List.length_tail, Usa1996P6.headBit, Decidable.byContradiction and 7 more

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

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

14. lemma Usa1996P6.binary_pair_unique line 165 source

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

    Statement uses: List, Fin, OfNat.ofNat, Nat, Eq, Int, HAdd.hAdd, Usa1996P6.negFourValue, HMul.hMul, And

    Proof uses: Usa1996P6.binary_pair_unique_aux, List.length, le_rfl

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

15. determine Usa1996P6.does_exist line 174 source

    no axioms what this means

    Statement uses: Bool

    Proof uses: Bool.true

16. problem Usa1996P6.usa1996_p6 line 176 source

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

    Statement uses: Iff, Eq, Bool, Usa1996P6.does_exist, Bool.true, Exists, Set, Int, Usa1996P6.UniqueRepresentationSet

    Proof uses: Eq.mpr, id, Eq.trans, True, congrFun', congrArg, eq_self, true_iff, Set.range, List, Fin, OfNat.ofNat, Nat, Usa1996P6.negFourValue, Exists.intro, ExistsUnique, Prod, And, Membership.mem, Prod.fst and 17 more

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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