[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]


[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g1 g2 : G
p : P
h : g1 +ᵥ p = g2 +ᵥ p
⊢ g1 = g2
[PROOFSTEP]
rw [← vadd_vsub g1 p, h, vadd_vsub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p1 p2 : P
⊢ g +ᵥ p1 -ᵥ p2 = g + (p1 -ᵥ p2)
[PROOFSTEP]
apply vadd_right_cancel p2
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p1 p2 : P
⊢ g +ᵥ p1 -ᵥ p2 +ᵥ p2 = g + (p1 -ᵥ p2) +ᵥ p2
[PROOFSTEP]
rw [vsub_vadd, add_vadd, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p : P
⊢ p -ᵥ p = 0
[PROOFSTEP]
rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
h : p1 -ᵥ p2 = 0
⊢ p1 = p2
[PROOFSTEP]
rw [← vsub_vadd p1 p2, h, zero_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3
[PROOFSTEP]
apply vadd_right_cancel p3
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p3) +ᵥ p3 = p1 -ᵥ p3 +ᵥ p3
[PROOFSTEP]
rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
⊢ -(p1 -ᵥ p2) = p2 -ᵥ p1
[PROOFSTEP]
refine' neg_eq_of_add_eq_zero_right (vadd_right_cancel p1 _)
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p1) +ᵥ p1 = 0 +ᵥ p1
[PROOFSTEP]
rw [vsub_add_vsub_cancel, vsub_self]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p q : P
⊢ g +ᵥ p -ᵥ q = g - (q -ᵥ p)
[PROOFSTEP]
rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
g : G
⊢ p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g
[PROOFSTEP]
rw [← add_right_inj (p2 -ᵥ p1 : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ← add_sub_assoc, ←
  neg_vsub_eq_vsub_rev, neg_add_self, zero_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p3 - (p2 -ᵥ p3) = p1 -ᵥ p2
[PROOFSTEP]
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
[PROOFSTEP]
rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p : P
⊢ {p} -ᵥ {p} = {0}
[PROOFSTEP]
rw [Set.singleton_vsub_singleton, vsub_self]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
⊢ v₁ +ᵥ p -ᵥ (v₂ +ᵥ p) = v₁ - v₂
[PROOFSTEP]
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p : P
h : p1 -ᵥ p = p2 -ᵥ p
⊢ p1 = p2
[PROOFSTEP]
rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p : P
h : p -ᵥ p1 = p -ᵥ p2
⊢ p1 = p2
[PROOFSTEP]
refine' vadd_left_cancel (p -ᵥ p2) _
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p : P
h : p -ᵥ p1 = p -ᵥ p2
⊢ p -ᵥ p2 +ᵥ p1 = p -ᵥ p2 +ᵥ p2
[PROOFSTEP]
rw [vsub_vadd, ← h, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p3 -ᵥ p2 - (p3 -ᵥ p1) = p1 -ᵥ p2
[PROOFSTEP]
rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v : G
p1 p2 : P
⊢ v +ᵥ p1 -ᵥ (v +ᵥ p2) = p1 -ᵥ p2
[PROOFSTEP]
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel']
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 +ᵥ p3 = p3 -ᵥ p2 +ᵥ p1
[PROOFSTEP]
rw [← @vsub_eq_zero_iff_eq G, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p3 -ᵥ p1 - (p3 -ᵥ p2)) = 0
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
[PROOFSTEP]
rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p₁ p₂ p₃ p₄ : P
⊢ p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
[PROOFSTEP]
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
p p' : P
⊢ (fun v => -v +ᵥ p) ((fun x x_1 => x -ᵥ x_1) p p') = p'
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
p : P
v : G
⊢ (fun x x_1 => x -ᵥ x_1) p ((fun v => -v +ᵥ p) v) = v
[PROOFSTEP]
simp [vsub_vadd_eq_vsub_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
v : G
p : P
⊢ (fun x x_1 => x +ᵥ x_1) (-v) ((fun x x_1 => x +ᵥ x_1) v p) = p
[PROOFSTEP]
simp [vadd_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
v : G
p : P
⊢ (fun x x_1 => x +ᵥ x_1) v ((fun x x_1 => x +ᵥ x_1) (-v) p) = p
[PROOFSTEP]
simp [vadd_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ -(x -ᵥ ↑(pointReflection x) y) = -(y -ᵥ x)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ ↑(pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)
[PROOFSTEP]
simp [pointReflection, two_nsmul, vadd_vsub_assoc]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ -(y -ᵥ ↑(pointReflection x) y) = -(2 • (y -ᵥ x))
[PROOFSTEP]
simp [← neg_nsmul]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x : P
⊢ ∀ (x_1 : P), ↑(pointReflection x).symm x_1 = ↑(pointReflection x) x_1
[PROOFSTEP]
simp [pointReflection]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ ↑(pointReflection x) y = ↑(pointReflection x).symm y
[PROOFSTEP]
rw [pointReflection_symm]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
h : Injective bit0
⊢ ↑(pointReflection x) y = y ↔ y = x
[PROOFSTEP]
rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero, ← bit0, ←
  bit0_zero, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
[GOAL]
G✝ : Type u_1
P✝ : Type u_2
inst✝³ : AddGroup G✝
inst✝² : AddTorsor G✝ P✝
G : Type u_3
P : Type u_4
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective bit0
y x₁ x₂ : P
hy : ↑(pointReflection x₁) y = ↑(pointReflection x₂) y
⊢ x₁ = x₂
[PROOFSTEP]
rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub, vsub_sub_vsub_cancel_right, ←
  neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero, ← bit0, ← bit0_zero, h.eq_iff, vsub_eq_zero_iff_eq] at hy
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
⊢ Subsingleton G ↔ Subsingleton P
[PROOFSTEP]
inhabit P
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
inhabited_h : Inhabited P
⊢ Subsingleton G ↔ Subsingleton P
[PROOFSTEP]
exact (Equiv.vaddConst default).subsingleton_congr


[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift #{ x // IsAlgebraic R x } ≤ lift #R[X] * ℵ₀
[PROOFSTEP]
rw [← mk_uLift, ← mk_uLift]
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #(ULift { x // IsAlgebraic R x }) ≤ #(ULift R[X]) * ℵ₀
[PROOFSTEP]
choose g hg₁ hg₂ using fun x : {x : A | IsAlgebraic R x} => x.coe_prop
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
⊢ #(ULift { x // IsAlgebraic R x }) ≤ #(ULift R[X]) * ℵ₀
[PROOFSTEP]
refine' lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le g fun f => _
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ lift #↑(g ⁻¹' {f}) ≤ ℵ₀
[PROOFSTEP]
rw [lift_le_aleph0, le_aleph0_iff_set_countable]
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ Set.Countable (g ⁻¹' {f})
[PROOFSTEP]
suffices : MapsTo (↑) (g ⁻¹' { f }) (f.rootSet A)
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
this : MapsTo Subtype.val (g ⁻¹' {f}) (rootSet f A)
⊢ Set.Countable (g ⁻¹' {f})
case this
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ MapsTo Subtype.val (g ⁻¹' {f}) (rootSet f A)
[PROOFSTEP]
exact this.countable_of_injOn (Subtype.coe_injective.injOn _) (f.rootSet_finite A).countable
[GOAL]
case this
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
f : R[X]
⊢ MapsTo Subtype.val (g ⁻¹' {f}) (rootSet f A)
[PROOFSTEP]
rintro x (rfl : g x = f)
[GOAL]
case this
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), ↑(aeval ↑x) (g x) = 0
x : ↑{x | IsAlgebraic R x}
⊢ ↑x ∈ rootSet (g x) A
[PROOFSTEP]
exact mem_rootSet.2 ⟨hg₁ x, hg₂ x⟩
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift (max #R ℵ₀) * ℵ₀ ≤ max (lift #R) ℵ₀
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ Set.Countable {x | IsAlgebraic R x}
[PROOFSTEP]
rw [← le_aleph0_iff_set_countable, ← lift_le]
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ lift #↑{x | IsAlgebraic R x} ≤ lift ℵ₀
[PROOFSTEP]
apply (cardinal_mk_lift_le_max R A).trans
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ max (lift #R) ℵ₀ ≤ lift ℵ₀
[PROOFSTEP]
simp
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀
[PROOFSTEP]
rw [← lift_id #_, ← lift_id #(R[X])]
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift #{ x // IsAlgebraic R x } ≤ lift #R[X] * ℵ₀
[PROOFSTEP]
exact cardinal_mk_lift_le_mul R A
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #{ x // IsAlgebraic R x } ≤ max #R ℵ₀
[PROOFSTEP]
rw [← lift_id #_, ← lift_id #R]
[GOAL]
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift #{ x // IsAlgebraic R x } ≤ max (lift #R) ℵ₀
[PROOFSTEP]
exact cardinal_mk_lift_le_max R A