case h
X : Type u_1
M : Type ?u.390661
R : Type u_2
𝕜 : Type ?u.390667
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
a✝ : X
⊢ ↑↑(↑unitsLift (unitsOfForallIsUnit h)) a✝ = ↑f a✝
X : Type u_1
M : Type ?u.390661
R : Type u_2
𝕜 : Type ?u.390667
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ ↑(↑unitsLift (unitsOfForallIsUnit h)) = f
ext
no goals
case h
X : Type u_1
M : Type ?u.390661
R : Type u_2
𝕜 : Type ?u.390667
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
a✝ : X
⊢ ↑↑(↑unitsLift (unitsOfForallIsUnit h)) a✝ = ↑f a✝
rfl