FormalConjecturesForMathlib/Combinatorics/Additive/VCDim.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def HasMulVCDimAtMost line 44 source

   no axioms what this means

   Statement uses: CommGroup, Set, Nat

   Proof uses: Fin, HAdd.hAdd, OfNat.ofNat, Not, Iff, Membership.mem, HMul.hMul

   11 instances, coercions and auxiliary constants left out.

2. lemma HasMulVCDimAtMost.mono line 48 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: CommGroup, Set, Nat, LE.le, HasMulVCDimAtMost

   Proof uses: Fin, HAdd.hAdd, OfNat.ofNat, Iff, Membership.mem, HMul.hMul, Decidable.byContradiction, Not, Function.comp, Fin.castLE, Set.image, Iff.trans, of_eq_true, Eq.trans, True, congrFun', congrArg, Exists, And, Eq and 2 more

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

3. lemma hasMulVCDimAtMost_compl line 55 source

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

   Statement uses: CommGroup, Set, Nat, Iff, HasMulVCDimAtMost, Compl.compl

   Proof uses: forall_congr', Fin, HAdd.hAdd, OfNat.ofNat, Not, Membership.mem, HMul.hMul, Equiv.forall_congr, Equiv.arrowCongr, Function.Involutive.toPerm, compl_involutive, Equiv.refl, not_congr, Equiv, Eq.mpr, id, Eq, forall_congr, congr, congrArg and 15 more

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

4. lemma HasMulVCDimAtMost.empty line 63 source

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

   Statement uses: CommGroup, Nat, HasMulVCDimAtMost, EmptyCollection.emptyCollection, Set

   Proof uses: Eq.mpr, Exists, Fin, HAdd.hAdd, OfNat.ofNat, Membership.mem, id, Eq, Eq.trans, Not, Iff, HMul.hMul, forall_congr, congrArg, False, congrFun', false_iff, funext, Exists.intro, Inhabited.default and 2 more

   29 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

5. lemma HasMulVCDimAtMost.univ line 67 source

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

   Statement uses: CommGroup, Nat, HasMulVCDimAtMost, Set.univ

   Proof uses: Eq.mpr, Exists, Fin, HAdd.hAdd, OfNat.ofNat, Set, Not, Membership.mem, id, Eq, Eq.trans, Iff, HMul.hMul, forall_congr, congrArg, True, congrFun', true_iff, funext, Exists.intro and 5 more

   27 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

6. lemma hasVCDimAtMost_smul line 71 source

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

   Statement uses: CommGroup, Set, Nat, Iff, HasVCDimAtMost, Set.ofPred, Exists, Eq, HSMul.hSMul, HasMulVCDimAtMost

   Proof uses: Eq.mpr, Fin, HAdd.hAdd, OfNat.ofNat, Not, Membership.mem, HMul.hMul, Inv.inv, id, congr, congrArg, forall_congr, Eq.trans, implies_congr, propext, Classical.skolem, funext, congrFun', forall_congr', Equiv.forall_congr and 7 more

   41 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

7. def HasMulVCNDimAtMost line 84 source

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

   Statement uses: CommGroup, Set, Nat

   Proof uses: Fin, HAdd.hAdd, OfNat.ofNat, Not, Iff, Membership.mem, HMul.hMul, Finset.prod, Finset.univ

   13 instances, coercions and auxiliary constants left out.

8. lemma HasMulVCNDimAtMost.mono line 89 source

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

   Statement uses: CommGroup, Set, Nat, LE.le, HasMulVCNDimAtMost

   Proof uses: Fin, HAdd.hAdd, OfNat.ofNat, Iff, Membership.mem, HMul.hMul, Finset.prod, Finset.univ, Decidable.byContradiction, Not, Function.comp, Fin.castLE, Set.image, Iff.trans, Eq.mpr, Exists, And, Eq, id, congrFun' and 7 more

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 6 steps

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

9. lemma hasMulVCNDimAtMost_compl line 97 source

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

   Statement uses: CommGroup, Set, Nat, Iff, HasMulVCNDimAtMost, Compl.compl

   Proof uses: forall_congr', Fin, HAdd.hAdd, OfNat.ofNat, Not, Membership.mem, HMul.hMul, Finset.prod, Finset.univ, Equiv.forall_congr, Equiv.arrowCongr, Function.Involutive.toPerm, compl_involutive, Equiv.refl, not_congr, Equiv, Eq.mpr, id, Eq, forall_congr and 17 more

   24 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

10. lemma HasMulVCNDimAtMost.empty line 105 source

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

    Statement uses: CommGroup, Nat, HasMulVCNDimAtMost, EmptyCollection.emptyCollection, Set

    Proof uses: Eq.mpr, Exists, Fin, HAdd.hAdd, OfNat.ofNat, Membership.mem, id, Eq, Eq.trans, Not, Iff, HMul.hMul, Finset.prod, Finset.univ, forall_congr, congrArg, False, congrFun', false_iff, funext and 4 more

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

11. lemma HasMulVCNDimAtMost.univ line 109 source

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

    Statement uses: CommGroup, Nat, HasMulVCNDimAtMost, Set.univ

    Proof uses: Eq.mpr, Exists, Fin, HAdd.hAdd, OfNat.ofNat, Set, Not, Membership.mem, id, Eq, Eq.trans, Iff, HMul.hMul, Finset.prod, Finset.univ, forall_congr, congrArg, True, congrFun', true_iff and 7 more

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

12. lemma hasMulVCNDimAtMost_zero line 113 source

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

    Statement uses: CommGroup, Set, Nat, Iff, HasMulVCNDimAtMost, OfNat.ofNat, Or, Eq, EmptyCollection.emptyCollection, Set.univ

    Proof uses: Iff.intro, Eq.mpr, Membership.mem, id, congrArg, propext, Set.eq_univ_iff_forall, Mathlib.Tactic.Contrapose.contrapose₁, Fin, HAdd.hAdd, Exists, Not, finZeroElim, And, Set.Nonempty, implies_congr, Eq.trans, congr, Mathlib.Tactic.Push.not_forall_eq, funext and 31 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

13. lemma hasMulVCNDimAtMost_one line 130 source

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

    Statement uses: CommGroup, Set, Nat, Iff, HasMulVCNDimAtMost, OfNat.ofNat, HasMulVCDimAtMost

    Proof uses: Iff.symm, Equiv.forall_congr, Fin, HAdd.hAdd, Not, Membership.mem, HMul.hMul, Finset.prod, Finset.univ, Equiv.symm, Equiv.funUnique, Equiv, Equiv.arrowCongr, Equiv.Set.congr, Equiv.refl, not_congr, of_eq_true, Eq.trans, True, congrArg and 28 more

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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