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).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ (subtypeCongr ep en).trans (subtypeCongr ep' en') = subtypeCongr (ep.trans ep') (en.trans en')
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).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) 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).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) 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).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) 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 { val := x, property := h })
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) 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).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
have : p (ep ⟨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 { val := x, property := h })
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
simp [Perm.subtypeCongr.apply, h, 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 { val := x, property := h })
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) 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).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
have : ¬p (en ⟨x, h⟩) := Subtype.property (en _)
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 { val := x, property := h })
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]