α : Type u_1
β : Type ?u.152201
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(subtypeCongr e (toCompl e)) x = ↑(↑e { val := x, property := hx })
α : Type u_1
β : Type ?u.152201
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(extendSubtype e) x = ↑(↑e { val := x, property := hx })
dsimp only [extendSubtype]
α : Type u_1
β : Type ?u.152201
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(sumCompl fun x => q x) (Sum.map (↑e) (↑(toCompl e)) (↑(sumCompl fun x => p x).symm x)) =
    ↑(↑e { val := x, property := hx })
α : Type u_1
β : Type ?u.152201
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(subtypeCongr e (toCompl e)) x = ↑(↑e { val := x, property := hx })
simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]
no goals
α : Type u_1
β : Type ?u.152201
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(sumCompl fun x => q x) (Sum.map (↑e) (↑(toCompl e)) (↑(sumCompl fun x => p x).symm x)) =
    ↑(↑e { val := x, property := hx })
rw [sumCompl_apply_symm_of_pos _ _ hx, Sum.map_inl, sumCompl_apply_inl]