case H
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ ↑(subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = ↑(Equiv.refl ε) x
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε
ext x
no goals
case H
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ ↑(subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = ↑(Equiv.refl ε) x
by_cases h:p x <;> simp [h]