FormalConjecturesForMathlib/Data/Sym/Sym2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Sym2.fst_out_mk_self line 25 source

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

   Statement uses: Eq, Prod.fst, Quot.out, Prod, Sym2.Rel, Sym2.mk

   Proof uses: Eq.mp, Membership.mem, Sym2, Eq.trans, Or, or_self, Sym2.out_fst_mem

   3 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

2. lemma Sym2.snd_out_mk_self line 26 source

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

   Statement uses: Eq, Prod.snd, Quot.out, Prod, Sym2.Rel, Sym2.mk

   Proof uses: Eq.mp, Membership.mem, Sym2, Eq.trans, Or, or_self, Sym2.out_snd_mem

   3 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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