[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : Mul β
inst✝ : ContinuousMul β
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
refine' continuous_of_continuous_uncurry _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : Mul β
inst✝ : ContinuousMul β
⊢ Continuous (Function.uncurry fun x y => ↑(x.fst * x.snd) y)
[PROOFSTEP]
have h1 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.fst x.snd :=
  continuous_eval'.comp (continuous_fst.prod_map continuous_id)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : Mul β
inst✝ : ContinuousMul β
h1 : Continuous fun x => ↑x.fst.fst x.snd
⊢ Continuous (Function.uncurry fun x y => ↑(x.fst * x.snd) y)
[PROOFSTEP]
have h2 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.snd x.snd :=
  continuous_eval'.comp (continuous_snd.prod_map continuous_id)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : Mul β
inst✝ : ContinuousMul β
h1 : Continuous fun x => ↑x.fst.fst x.snd
h2 : Continuous fun x => ↑x.fst.snd x.snd
⊢ Continuous (Function.uncurry fun x y => ↑(x.fst * x.snd) y)
[PROOFSTEP]
exact h1.mul h2
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
ι : Type u_3
s : Finset ι
f : ι → C(α, β)
a : α
⊢ ↑(∏ i in s, f i) a = ∏ i in s, ↑(f i) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
letI : UniformSpace β := TopologicalGroup.toUniformSpace β
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this : UniformSpace β := TopologicalGroup.toUniformSpace β
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
have : UniformGroup β := comm_topologicalGroup_is_uniform
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
⊢ ∀ (x : C(α, β) × C(α, β)), ContinuousAt (fun p => p.fst * p.snd) x
[PROOFSTEP]
rintro ⟨f, g⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
f g : C(α, β)
⊢ ContinuousAt (fun p => p.fst * p.snd) (f, g)
[PROOFSTEP]
rw [ContinuousAt, tendsto_iff_forall_compact_tendstoUniformlyOn, nhds_prod_eq]
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
f g : C(α, β)
⊢ ∀ (K : Set α),
    IsCompact K → TendstoUniformlyOn (fun i a => ↑(i.fst * i.snd) a) (↑((f, g).fst * (f, g).snd)) (nhds f ×ˢ nhds g) K
[PROOFSTEP]
exact fun K hK =>
  uniformContinuous_mul.comp_tendstoUniformlyOn
    ((tendsto_iff_forall_compact_tendstoUniformlyOn.mp Filter.tendsto_id K hK).prod
      (tendsto_iff_forall_compact_tendstoUniformlyOn.mp Filter.tendsto_id K hK))
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
⊢ Continuous fun a => a⁻¹
[PROOFSTEP]
letI : UniformSpace β := TopologicalGroup.toUniformSpace β
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this : UniformSpace β := TopologicalGroup.toUniformSpace β
⊢ Continuous fun a => a⁻¹
[PROOFSTEP]
have : UniformGroup β := comm_topologicalGroup_is_uniform
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
⊢ Continuous fun a => a⁻¹
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
⊢ ∀ (x : C(α, β)), ContinuousAt (fun a => a⁻¹) x
[PROOFSTEP]
intro f
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
f : C(α, β)
⊢ ContinuousAt (fun a => a⁻¹) f
[PROOFSTEP]
rw [ContinuousAt, tendsto_iff_forall_compact_tendstoUniformlyOn]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : TopologicalGroup β
this✝ : UniformSpace β := TopologicalGroup.toUniformSpace β
this : UniformGroup β
f : C(α, β)
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑i⁻¹ a) (↑f⁻¹) (nhds f) K
[PROOFSTEP]
exact fun K hK =>
  uniformContinuous_inv.comp_tendstoUniformlyOn
    (tendsto_iff_forall_compact_tendstoUniformlyOn.mp Filter.tendsto_id K hK)
      -- TODO: rewrite the next three lemmas for products and deduce sum case via `to_additive`, once
      -- definition of `tprod` is in place
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : AddCommMonoid β
inst✝ : ContinuousAdd β
f : γ → C(α, β)
g : C(α, β)
hf : HasSum f g
x : α
⊢ HasSum (fun i => ↑(f i) x) (↑g x)
[PROOFSTEP]
let ev : C(α, β) →+ β := (Pi.evalAddMonoidHom _ x).comp coeFnAddMonoidHom
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : AddCommMonoid β
inst✝ : ContinuousAdd β
f : γ → C(α, β)
g : C(α, β)
hf : HasSum f g
x : α
ev : C(α, β) →+ β := AddMonoidHom.comp (Pi.evalAddMonoidHom (fun a => β) x) coeFnAddMonoidHom
⊢ HasSum (fun i => ↑(f i) x) (↑g x)
[PROOFSTEP]
exact hf.map ev (ContinuousMap.continuous_eval_const x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
R : Type u_3
R₁ : Type u_4
M : Type u_5
inst✝⁵ : TopologicalSpace M
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : LocallyCompactSpace α
inst✝² : TopologicalSpace R
inst✝¹ : SMul R M
inst✝ : ContinuousSMul R M
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
refine' continuous_of_continuous_uncurry _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
R : Type u_3
R₁ : Type u_4
M : Type u_5
inst✝⁵ : TopologicalSpace M
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : LocallyCompactSpace α
inst✝² : TopologicalSpace R
inst✝¹ : SMul R M
inst✝ : ContinuousSMul R M
⊢ Continuous (Function.uncurry fun x y => ↑(x.fst • x.snd) y)
[PROOFSTEP]
have h : Continuous fun x : (R × C(α, M)) × α => x.fst.snd x.snd :=
  continuous_eval'.comp (continuous_snd.prod_map continuous_id)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
R : Type u_3
R₁ : Type u_4
M : Type u_5
inst✝⁵ : TopologicalSpace M
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : LocallyCompactSpace α
inst✝² : TopologicalSpace R
inst✝¹ : SMul R M
inst✝ : ContinuousSMul R M
h : Continuous fun x => ↑x.fst.snd x.snd
⊢ Continuous (Function.uncurry fun x y => ↑(x.fst • x.snd) y)
[PROOFSTEP]
exact (continuous_fst.comp continuous_fst).smul h
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
⊢ (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1
[PROOFSTEP]
ext _
[GOAL]
case h
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
a✝ : α
⊢ ↑((fun c => mk fun x => ↑(algebraMap R A) c) 1) a✝ = ↑1 a✝
[PROOFSTEP]
exact (algebraMap R A).map_one
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c₁ c₂ : R
⊢ OneHom.toFun
      { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
        map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
      (c₁ * c₂) =
    OneHom.toFun
        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
        c₁ *
      OneHom.toFun
        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
        c₂
[PROOFSTEP]
ext _
[GOAL]
case h
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ ↑(OneHom.toFun
          { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
            map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
          (c₁ * c₂))
      a✝ =
    ↑(OneHom.toFun
            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
            c₁ *
          OneHom.toFun
            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
            c₂)
      a✝
[PROOFSTEP]
exact (algebraMap R A).map_mul _ _
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (c₁ c₂ : R),
                OneHom.toFun
                    { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                      map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                    (c₁ * c₂) =
                  OneHom.toFun
                      { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                        map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                      c₁ *
                    OneHom.toFun
                      { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                        map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                      c₂) })
      0 =
    0
[PROOFSTEP]
ext _
[GOAL]
case h
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
a✝ : α
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                  map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (c₁ c₂ : R),
                    OneHom.toFun
                        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                        (c₁ * c₂) =
                      OneHom.toFun
                          { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                            map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                          c₁ *
                        OneHom.toFun
                          { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                            map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                          c₂) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
exact (algebraMap R A).map_zero
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c₁ c₂ : R
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (c₁ c₂ : R),
                OneHom.toFun
                    { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                      map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                    (c₁ * c₂) =
                  OneHom.toFun
                      { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                        map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                      c₁ *
                    OneHom.toFun
                      { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                        map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                      c₂) })
      (c₁ + c₂) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (c₁ c₂ : R),
                  OneHom.toFun
                      { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                        map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                      (c₁ * c₂) =
                    OneHom.toFun
                        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                        c₁ *
                      OneHom.toFun
                        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                        c₂) })
        c₁ +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (c₁ c₂ : R),
                  OneHom.toFun
                      { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                        map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                      (c₁ * c₂) =
                    OneHom.toFun
                        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                        c₁ *
                      OneHom.toFun
                        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                        c₂) })
        c₂
[PROOFSTEP]
ext _
[GOAL]
case h
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                  map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (c₁ c₂ : R),
                    OneHom.toFun
                        { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                          map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                        (c₁ * c₂) =
                      OneHom.toFun
                          { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                            map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                          c₁ *
                        OneHom.toFun
                          { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                            map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                          c₂) })
          (c₁ + c₂))
      a✝ =
    ↑(OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                    map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (c₁ c₂ : R),
                      OneHom.toFun
                          { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                            map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                          (c₁ * c₂) =
                        OneHom.toFun
                            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                            c₁ *
                          OneHom.toFun
                            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                            c₂) })
            c₁ +
          OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                    map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (c₁ c₂ : R),
                      OneHom.toFun
                          { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                            map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                          (c₁ * c₂) =
                        OneHom.toFun
                            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                            c₁ *
                          OneHom.toFun
                            { toFun := fun c => mk fun x => ↑(algebraMap R A) c,
                              map_one' := (_ : (fun c => mk fun x => ↑(algebraMap R A) c) 1 = 1) }
                            c₂) })
            c₂)
      a✝
[PROOFSTEP]
exact (algebraMap R A).map_add _ _
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c : R
f : (fun x => C(α, A)) c
⊢ ↑C c * f = f * ↑C c
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c : R
f : (fun x => C(α, A)) c
x : α
⊢ ↑(↑C c * f) x = ↑(f * ↑C c) x
[PROOFSTEP]
exact Algebra.commutes' _ _
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c : R
f : (fun x => C(α, A)) c
⊢ c • f = ↑C c * f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
c : R
f : (fun x => C(α, A)) c
x : α
⊢ ↑(c • f) x = ↑(↑C c * f) x
[PROOFSTEP]
exact Algebra.smul_def' _ _
[GOAL]
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
⊢ (fun g => comp g f) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
a✝ : α
⊢ ↑((fun g => comp g f) 1) a✝ = ↑1 a✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
g₁ g₂ : C(β, A)
⊢ OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂) =
    OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
g₁ g₂ : C(β, A)
a✝ : α
⊢ ↑(OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂)) a✝ =
    ↑(OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
          OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂)
      a✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (g₁ g₂ : C(β, A)),
                OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂) =
                  OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                    OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
a✝ : α
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (g₁ g₂ : C(β, A)),
                    OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂) =
                      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                        OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
g₁ g₂ : C(β, A)
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (g₁ g₂ : C(β, A)),
                OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂) =
                  OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                    OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
      (g₁ + g₂) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (g₁ g₂ : C(β, A)),
                  OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂) =
                    OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
        g₁ +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (g₁ g₂ : C(β, A)),
                  OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂) =
                    OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
        g₂
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
g₁ g₂ : C(β, A)
a✝ : α
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (g₁ g₂ : C(β, A)),
                    OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } (g₁ * g₂) =
                      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                        OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
          (g₁ + g₂))
      a✝ =
    ↑(OneHom.toFun
            (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (g₁ g₂ : C(β, A)),
                      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                          (g₁ * g₂) =
                        OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                          OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                            g₂) })
            g₁ +
          OneHom.toFun
            (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (g₁ g₂ : C(β, A)),
                      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                          (g₁ * g₂) =
                        OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                          OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                            g₂) })
            g₂)
      a✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (g₁ g₂ : C(β, A)),
                      OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                          (g₁ * g₂) =
                        OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                          OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                            g₂) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (g₁ g₂ : C(β, A)),
                              OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                  (g₁ * g₂) =
                                OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                    g₁ *
                                  OneHom.toFun
                                    { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (g₁ g₂ : C(β, A)),
                  OneHom.toFun
                      (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (g₁ g₂ : C(β, A)),
                                OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                    (g₁ * g₂) =
                                  OneHom.toFun
                                      { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                                    OneHom.toFun
                                      { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₂) })
                      (g₁ + g₂) =
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (g₁ g₂ : C(β, A)),
                                  OneHom.toFun
                                      { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                      (g₁ * g₂) =
                                    OneHom.toFun
                                        { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                                      OneHom.toFun
                                        { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                        g₂) })
                        g₁ +
                      OneHom.toFun
                        (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (g₁ g₂ : C(β, A)),
                                  OneHom.toFun
                                      { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                      (g₁ * g₂) =
                                    OneHom.toFun
                                        { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                                      OneHom.toFun
                                        { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                        g₂) })
                        g₂) })
      (↑(algebraMap R C(β, A)) r) =
    ↑(algebraMap R C(α, A)) r
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
inst✝¹¹ : TopologicalSpace α✝
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁵ : TopologicalSpace A₂
inst✝⁴ : Semiring A₂
inst✝³ : Algebra R A₂
inst✝² : TopologicalSemiring A₂
α : Type u_5
β : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : C(α, β)
r : R
a✝ : α
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  { toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (g₁ g₂ : C(β, A)),
                          OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                              (g₁ * g₂) =
                            OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                g₁ *
                              OneHom.toFun { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                g₂) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (g₁ g₂ : C(β, A)),
                                  OneHom.toFun
                                      { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                      (g₁ * g₂) =
                                    OneHom.toFun
                                        { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) } g₁ *
                                      OneHom.toFun
                                        { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                        g₂) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (g₁ g₂ : C(β, A)),
                      OneHom.toFun
                          (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (g₁ g₂ : C(β, A)),
                                    OneHom.toFun
                                        { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                        (g₁ * g₂) =
                                      OneHom.toFun
                                          { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                          g₁ *
                                        OneHom.toFun
                                          { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                          g₂) })
                          (g₁ + g₂) =
                        OneHom.toFun
                            (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (g₁ g₂ : C(β, A)),
                                      OneHom.toFun
                                          { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                          (g₁ * g₂) =
                                        OneHom.toFun
                                            { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                            g₁ *
                                          OneHom.toFun
                                            { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                            g₂) })
                            g₁ +
                          OneHom.toFun
                            (↑{ toOneHom := { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (g₁ g₂ : C(β, A)),
                                      OneHom.toFun
                                          { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                          (g₁ * g₂) =
                                        OneHom.toFun
                                            { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                            g₁ *
                                          OneHom.toFun
                                            { toFun := fun g => comp g f, map_one' := (_ : (fun g => comp g f) 1 = 1) }
                                            g₂) })
                            g₂) })
          (↑(algebraMap R C(β, A)) r))
      a✝ =
    ↑(↑(algebraMap R C(α, A)) r) a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
[PROOFSTEP]
obtain ⟨f, m, w⟩ := h n
[GOAL]
case intro.intro
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
f : α → A
m : f ∈ (fun f => ↑f) '' ↑s
w : f x ≠ f y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
[PROOFSTEP]
rcases m with ⟨f, ⟨m, rfl⟩⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
f : C(α, A)
m : f ∈ ↑s
w : (fun f => ↑f) f x ≠ (fun f => ↑f) f y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
[PROOFSTEP]
exact ⟨_, ⟨f, ⟨r m, rfl⟩⟩, w⟩
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
k : R
a : α
⊢ ↑(↑(algebraMap R C(α, A)) k) a = k • 1
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one]
[GOAL]
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
k : R
a : α
⊢ ↑(k • 1) a = k • 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
by_cases n : x = y
[GOAL]
case pos
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : x = y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
subst n
[GOAL]
case pos
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x : α
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f x = v x
[PROOFSTEP]
refine' ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩
[GOAL]
case neg
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
obtain ⟨_, ⟨f, hf, rfl⟩, hxy⟩ := h n
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : (fun f => ↑f) f x ≠ (fun f => ↑f) f y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
replace hxy : f x - f y ≠ 0 := sub_ne_zero_of_ne hxy
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
let a := v x
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
let b := v y
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
let f' : s := ((b - a) * (f x - f y)⁻¹) • (algebraMap _ s (f x) - (⟨f, hf⟩ : s)) + algebraMap _ s a
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
[PROOFSTEP]
refine' ⟨f', f'.prop, _, _⟩
[GOAL]
case neg.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ↑↑f' x = v x
[PROOFSTEP]
simp
[GOAL]
case neg.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹² : TopologicalSpace α
R : Type u_2
inst✝¹¹ : CommSemiring R
A : Type u_3
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type u_4
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ↑↑f' y = v y
[PROOFSTEP]
simp [inv_mul_cancel_right₀ hxy]
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
⊢ s₁ = s₂
[PROOFSTEP]
cases isEmpty_or_nonempty α
[GOAL]
case inl
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : IsEmpty α
⊢ s₁ = s₂
[PROOFSTEP]
haveI : Subsingleton C(α, R) := FunLike.coe_injective.subsingleton
[GOAL]
case inl
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : IsEmpty α
this : Subsingleton C(α, R)
⊢ s₁ = s₂
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
⊢ s₁ = s₂
[PROOFSTEP]
inhabit α
[GOAL]
case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ s₁ = s₂
[PROOFSTEP]
ext f
[GOAL]
case inr.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
⊢ f ∈ s₁ ↔ f ∈ s₂
[PROOFSTEP]
have h : f = algebraMap R C(α, R) (f default) := by
  ext x'
  simp only [mul_one, Algebra.id.smul_eq_mul, algebraMap_apply]
  congr
  simp
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
⊢ f = ↑(algebraMap R C(α, R)) (↑f default)
[PROOFSTEP]
ext x'
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
⊢ ↑f x' = ↑(↑(algebraMap R C(α, R)) (↑f default)) x'
[PROOFSTEP]
simp only [mul_one, Algebra.id.smul_eq_mul, algebraMap_apply]
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
⊢ ↑f x' = ↑f default
[PROOFSTEP]
congr
[GOAL]
case h.h.e_6.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
⊢ x' = default
[PROOFSTEP]
simp
[GOAL]
case inr.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h : f = ↑(algebraMap R C(α, R)) (↑f default)
⊢ f ∈ s₁ ↔ f ∈ s₂
[PROOFSTEP]
rw [h]
[GOAL]
case inr.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h : f = ↑(algebraMap R C(α, R)) (↑f default)
⊢ ↑(algebraMap R C(α, R)) (↑f default) ∈ s₁ ↔ ↑(algebraMap R C(α, R)) (↑f default) ∈ s₂
[PROOFSTEP]
simp only [Subalgebra.algebraMap_mem]
[GOAL]
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : C(α, M)
⊢ 1 • f = f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : C(α, M)
x : α
⊢ ↑(1 • f) x = ↑f x
[PROOFSTEP]
exact one_smul R (f x)
[GOAL]
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
c₁ c₂ : C(α, R)
f : C(α, M)
⊢ (c₁ * c₂) • f = c₁ • c₂ • f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ ↑((c₁ * c₂) • f) x = ↑(c₁ • c₂ • f) x
[PROOFSTEP]
exact mul_smul (c₁ x) (c₂ x) (f x)
[GOAL]
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
r : C(α, R)
⊢ r • 0 = 0
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
r : C(α, R)
x : α
⊢ ↑(r • 0) x = ↑0 x
[PROOFSTEP]
exact smul_zero _
[GOAL]
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
c : C(α, R)
f g : C(α, M)
⊢ c • (f + g) = c • f + c • g
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
c : C(α, R)
f g : C(α, M)
x : α
⊢ ↑(c • (f + g)) x = ↑(c • f + c • g) x
[PROOFSTEP]
exact smul_add (c x) (f x) (g x)
[GOAL]
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
c₁ c₂ : C(α, R)
f : C(α, M)
⊢ (c₁ + c₂) • f = c₁ • f + c₂ • f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ ↑((c₁ + c₂) • f) x = ↑(c₁ • f + c₂ • f) x
[PROOFSTEP]
exact add_smul (c₁ x) (c₂ x) (f x)
[GOAL]
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : C(α, M)
⊢ 0 • f = 0
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : C(α, M)
x : α
⊢ ↑(0 • f) x = ↑0 x
[PROOFSTEP]
exact zero_smul _ _
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p : X
⊢ Function.Periodic (↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p)))) p
[PROOFSTEP]
intro x
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
[PROOFSTEP]
by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
[PROOFSTEP]
convert congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1
  -- Porting note: in mathlib3 the proof from here was:
      -- simp_rw [←tsum_apply h, ←tsum_apply ((equiv.add_right (1 : ℤ)).summable_iff.mpr h),
      --   equiv.coe_add_right, comp_apply, coe_add_right, add_one_zsmul, add_comm (_ • p) p,
      --   ←add_assoc]
      -- However now the second `←tsum_apply` doesn't fire unless we use `erw`.
[GOAL]
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (c : ℤ), comp f (ContinuousMap.addRight (↑(Equiv.addRight 1) c • p))) x
[PROOFSTEP]
simp_rw [← tsum_apply h]
[GOAL]
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ∑' (i : ℤ), ↑(comp f (ContinuousMap.addRight (i • p))) (x + p) =
    ↑(∑' (c : ℤ), comp f (ContinuousMap.addRight (↑(Equiv.addRight 1) c • p))) x
[PROOFSTEP]
erw [← tsum_apply ((Equiv.addRight (1 : ℤ)).summable_iff.mpr h)]
[GOAL]
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ∑' (i : ℤ), ↑(comp f (ContinuousMap.addRight (i • p))) (x + p) =
    ∑' (i : ℤ), ↑(((fun n => comp f (ContinuousMap.addRight (n • p))) ∘ ↑(Equiv.addRight 1)) i) x
[PROOFSTEP]
simp [coe_addRight, add_one_zsmul, add_comm (_ • p) p, ← add_assoc]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable h]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : TopologicalSpace Y
inst✝¹² : TopologicalSpace Z
𝕜 : Type u_4
inst✝¹¹ : CommSemiring 𝕜
A : Type u_5
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : TopologicalSemiring A
inst✝⁷ : StarRing A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑0 (x + p) = ↑0 x
[PROOFSTEP]
simp only [coe_zero, Pi.zero_apply]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
𝕜 : Type u_3
inst✝⁶ : CommSemiring 𝕜
A : Type u_4
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : TopologicalSemiring A
inst✝² : StarRing A
inst✝¹ : ContinuousStar A
inst✝ : Algebra 𝕜 A
f : X ≃ₜ Y
src✝ : C(Y, A) →⋆ₐ[𝕜] C(X, A) := ContinuousMap.compStarAlgHom' 𝕜 A (toContinuousMap f)
g : C(Y, A)
⊢ ↑(ContinuousMap.compStarAlgHom' 𝕜 A (toContinuousMap (Homeomorph.symm f)))
      (↑(ContinuousMap.compStarAlgHom' 𝕜 A (toContinuousMap f)) g) =
    g
[PROOFSTEP]
simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc, toContinuousMap_comp_symm,
  ContinuousMap.comp_id]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
𝕜 : Type u_3
inst✝⁶ : CommSemiring 𝕜
A : Type u_4
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : TopologicalSemiring A
inst✝² : StarRing A
inst✝¹ : ContinuousStar A
inst✝ : Algebra 𝕜 A
f : X ≃ₜ Y
src✝ : C(Y, A) →⋆ₐ[𝕜] C(X, A) := ContinuousMap.compStarAlgHom' 𝕜 A (toContinuousMap f)
g : C(X, A)
⊢ ↑(ContinuousMap.compStarAlgHom' 𝕜 A (toContinuousMap f))
      (↑(ContinuousMap.compStarAlgHom' 𝕜 A (toContinuousMap (Homeomorph.symm f))) g) =
    g
[PROOFSTEP]
simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc, symm_comp_toContinuousMap,
  ContinuousMap.comp_id]
