[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, Mˣ)
⊢ (fun f =>
        mk fun x =>
          { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
            inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
      ((fun f =>
          { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
            val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
            inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h.a
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, Mˣ)
a✝ : X
⊢ ↑(↑((fun f =>
              mk fun x =>
                { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
                  inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
            ((fun f =>
                { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
                  val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
                  inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
              f))
        a✝) =
    ↑(↑f a✝)
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, M)ˣ
⊢ (fun f =>
        { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
          val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
          inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
      ((fun f =>
          mk fun x =>
            { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
              inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case a.h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, M)ˣ
a✝ : X
⊢ ↑↑((fun f =>
              { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
                val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
                inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
            ((fun f =>
                mk fun x =>
                  { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
                    inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
              f))
      a✝ =
    ↑↑f a✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, M)ˣ
x : X
⊢ ↑(↑(↑unitsLift.symm f) x)⁻¹ = ↑↑f⁻¹ x
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ Continuous fun x => IsUnit.unit (_ : IsUnit (↑f x))
[PROOFSTEP]
refine'
  continuous_induced_rng.2
    (Continuous.prod_mk f.continuous (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => _)))
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
[PROOFSTEP]
have := NormedRing.inverse_continuousAt (h x).unit
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
[PROOFSTEP]
simp only
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑(IsUnit.unit (_ : IsUnit (↑f x)))⁻¹) x
[PROOFSTEP]
simp only [← Ring.inverse_unit, IsUnit.unit_spec] at this ⊢
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse (↑f x)
⊢ ContinuousAt (fun x => Ring.inverse (↑f x)) x
[PROOFSTEP]
exact this.comp (f.continuousAt x)
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ (mk fun x => ↑(↑(unitsOfForallIsUnit h) x)) = f
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
a✝ : X
⊢ ↑(mk fun x => ↑(↑(unitsOfForallIsUnit h) x)) a✝ = ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ ↑(↑unitsLift (unitsOfForallIsUnit h)) = f
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
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✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ IsUnit f ↔ ∀ (x : X), ↑f x ≠ 0
[PROOFSTEP]
simp_rw [f.isUnit_iff_forall_isUnit, isUnit_iff_ne_zero]
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ spectrum 𝕜 f = Set.range ↑f
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
x : 𝕜
⊢ x ∈ spectrum 𝕜 f ↔ x ∈ Set.range ↑f
[PROOFSTEP]
simp only [spectrum.mem_iff, isUnit_iff_forall_ne_zero, not_forall, coe_sub, Pi.sub_apply, algebraMap_apply,
  Algebra.id.smul_eq_mul, mul_one, Classical.not_not, Set.mem_range, sub_eq_zero, @eq_comm _ x _]
