case H
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ (subtypeCongr ep en).symm = subtypeCongr ep.symm en.symm
ext x
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x

case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
case H
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
by_cases h:p x
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑(↑ep.symm { val := x, property := h })
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
have : p (ep.symm ⟨x, h⟩) := Subtype.property _
no goals
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑(↑ep.symm { val := x, property := h })
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑(↑en.symm { val := x, property := h })
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
have : ¬p (en.symm ⟨x, h⟩) := Subtype.property (en.symm _)
no goals
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑(↑en.symm { val := x, property := h })
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]