α : Type u_2
β : Type u_1
γ : Type ?u.48613
δ : Type ?u.48616
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ (e.source ∩ ↑e ⁻¹' s)
α : Type u_2
β : Type u_1
γ : Type ?u.48613
δ : Type ?u.48616
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set β
⊢ (LocalEquiv.trans e (LocalEquiv.restr (LocalEquiv.refl β) s)).source =
    (LocalEquiv.restr e (e.source ∩ ↑e ⁻¹' s)).source
simp [trans_source]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.48613
δ : Type ?u.48616
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ (e.source ∩ ↑e ⁻¹' s)
rw [← inter_assoc, inter_self]