case left
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = (LocalHomeomorph.restr e' e.source).toLocalEquiv.source

case right
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source))
    (LocalHomeomorph.restr e e'.source).toLocalEquiv.source
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ LocalHomeomorph.restr e e'.source ≈ LocalHomeomorph.restr e' e.source
constructor
case left
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = e'.source ∩ e.source
case left
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = (LocalHomeomorph.restr e' e.source).toLocalEquiv.source
rw [e'.restr_source' _ e.open_source]
case left
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source
case left
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = e'.source ∩ e.source
rw [e.restr_source' _ e'.open_source]
no goals
case left
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source
exact Set.inter_comm _ _
case right
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source)) (e.source ∩ e'.source)
case right
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source))
    (LocalHomeomorph.restr e e'.source).toLocalEquiv.source
rw [e.restr_source' _ e'.open_source]
no goals
case right
α : Type u_1
β : Type u_2
γ : Type ?u.81218
δ : Type ?u.81221
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source)) (e.source ∩ e'.source)
refine' (EqOn.trans _ h).trans _ <;> simp only [mfld_simps, eqOn_refl]