α : Type u_1
β : Type ?u.41041
γ : Type ?u.41044
δ : Type ?u.41047
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ univ ∩ id ⁻¹' s = s
α : Type u_1
β : Type ?u.41041
γ : Type ?u.41044
δ : Type ?u.41047
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ (LocalEquiv.restr (LocalEquiv.refl α) s).target = s
change univ ∩ id ⁻¹' s = s
no goals
α : Type u_1
β : Type ?u.41041
γ : Type ?u.41044
δ : Type ?u.41047
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ univ ∩ id ⁻¹' s = s
simp