PFR/Mathlib/Data/Fin/Basic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem Fin.cast_bijective line 7 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Eq, Function.Bijective, Fin, Fin.cast

   Proof uses: Eq.rec, Eq.mpr, Eq.refl, id, congrArg, Fin.cast_refl, Function.bijective_id

   Tactic trace: 2 steps

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

2. theorem Fin.cast_surjective line 10 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Eq, Function.Surjective, Fin, Fin.cast

   Proof uses: Function.Bijective.surjective, Fin.cast_bijective

3. theorem Fin.forall_fin_three line 13 source

   standard axioms: propext what this means

   Statement uses: Fin, OfNat.ofNat, Nat, Iff, And

   Proof uses: Iff.trans, HAdd.hAdd, Fin.succ, Fin.forall_fin_succ, and_congr_right, Fin.forall_fin_two

   9 instances, coercions and auxiliary constants left out.