[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α →CO β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : α →CO β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_open'✝ : IsOpenMap (ContinuousMap.mk toFun✝).toFun
h : (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ } = (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
map_open'✝¹ : IsOpenMap (ContinuousMap.mk toFun✝¹).toFun
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_open'✝ : IsOpenMap (ContinuousMap.mk toFun✝).toFun
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝¹, map_open' := map_open'✝¹ } =
    (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, map_open' := map_open'✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
