FormalConjecturesForMathlib/Order/Interval/Finset/Nat.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. theorem Nat.ncard_Iio line 25 source

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

    Statement uses: Nat, Eq, Set.ncard, Set.Iio

    Proof uses: Eq.mpr, Finset, Finset.Iio, id, congrArg, Set, Eq.symm, Finset.coe_Iio, Finset.card, Set.ncard_coe_finset, Nat.card_Iio

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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