α : Type u_1
β : Type ?u.49680
γ : Type ?u.49683
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o
α : Type u_1
β : Type ?u.49680
γ : Type ?u.49683
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o
rw [show f = id from funext H]
no goals
α : Type u_1
β : Type ?u.49680
γ : Type ?u.49683
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o
exact id_map o