FormalConjecturesForMathlib/Data/Finset/Card.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Finset.card_lt_card_iff_of_subset line 25 source

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

    Statement uses: Finset, LE.le, Iff, LT.lt, Nat, Finset.card, Ne

    Proof uses: Eq.mpr, Not, id, Eq, congrArg, Eq.symm, propext, not_le, Finset.eq_iff_card_le_of_subset, Iff.rfl

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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