case mk
α : Type u_2
β : Type u_1
γ : Type ?u.24772
δ : Type ?u.24775
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g✝ g : C(α, β)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : ↑(mk toFun✝) = ↑g
⊢ mk toFun✝ = g
α : Type u_2
β : Type u_1
γ : Type ?u.24772
δ : Type ?u.24775
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f✝ g✝ f g : C(α, β)
h : ↑f = ↑g
⊢ f = g
cases f
case mk.mk
α : Type u_2
β : Type u_1
γ : Type ?u.24772
δ : Type ?u.24775
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : ↑(mk toFun✝¹) = ↑(mk toFun✝)
⊢ mk toFun✝¹ = mk toFun✝
case mk
α : Type u_2
β : Type u_1
γ : Type ?u.24772
δ : Type ?u.24775
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g✝ g : C(α, β)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : ↑(mk toFun✝) = ↑g
⊢ mk toFun✝ = g
cases g
no goals
case mk.mk
α : Type u_2
β : Type u_1
γ : Type ?u.24772
δ : Type ?u.24775
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
h : ↑(mk toFun✝¹) = ↑(mk toFun✝)
⊢ mk toFun✝¹ = mk toFun✝
congr