α : Type u_1
β : Type u_2
γ : Type ?u.28742
δ : Type ?u.28745
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
⊢ (∀ (x : α), ↑e x = ↑e x) ∧
    (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e) x) ∧ e.source = e.source
α : Type u_1
β : Type u_2
γ : Type ?u.28742
δ : Type ?u.28745
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e e' : LocalHomeomorph α β
⊢ e = e' →
    (∀ (x : α), ↑e x = ↑e' x) ∧
      (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e') x) ∧ e.source = e'.source
rintro rfl
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.28742
δ : Type ?u.28745
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
⊢ (∀ (x : α), ↑e x = ↑e x) ∧
    (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e) x) ∧ e.source = e.source
exact ⟨fun x => rfl, fun x => rfl, rfl⟩