-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.subtypeCongr.trans :
    (ep.subtypeCongr en).trans (ep'.subtypeCongr en')
    = Perm.subtypeCongr (ep.trans ep') (en.trans en')

Proof state:
case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑(en ⟨x, h⟩)
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Tactic:
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]

Result:
no goals

Proof state:
case H
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Tactic:
by_cases h : p x

Result:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Proof state:
case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Tactic:
have : ¬p (en ⟨x, h⟩) := Subtype.property (en _)

Result:
case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑(en ⟨x, h⟩)
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Proof state:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Tactic:
have : p (ep ⟨x, h⟩) := Subtype.property _

Result:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑(ep ⟨x, h⟩)
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Proof state:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑(ep ⟨x, h⟩)
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x

Tactic:
simp [Perm.subtypeCongr.apply, h, this]

Result:
no goals

Proof state:
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') = subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')

Tactic:
ext x

Result:
case H
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ (Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en')) x =
    (subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')) x