case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ ↑(Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)).toSubsemiring
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈
    Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
⊢ ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S))
rintro _ ⟨f, hf, rfl⟩
case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ ↑(Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)).toSubsemiring
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈
    Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ ↑(Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)).toSubsemiring
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈
    Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
change _ ∈ (Algebra.adjoin 𝕜 S).restrictScalars ℝ
case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈
    Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ ↑(Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)).toSubsemiring
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈
    Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
change _ ∈ (Algebra.adjoin 𝕜 S).restrictScalars ℝ at hf
case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈
    Subalgebra.restrictScalars ℝ (Algebra.adjoin 𝕜 S)
rw [Subalgebra.mem_restrictScalars] at hf ⊢
case intro.intro.refine_1
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (x : C(X, 𝕜)), x ∈ S → ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) x ∈ Algebra.adjoin 𝕜 S

case intro.intro.refine_2
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (r : 𝕜),
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (↑(algebraMap 𝕜 C(X, 𝕜)) r) ∈ Algebra.adjoin 𝕜 S

case intro.intro.refine_3
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (x y : C(X, 𝕜)),
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) x ∈ Algebra.adjoin 𝕜 S →
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) y ∈ Algebra.adjoin 𝕜 S →
        ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (x + y) ∈ Algebra.adjoin 𝕜 S

case intro.intro.refine_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (x y : C(X, 𝕜)),
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) x ∈ Algebra.adjoin 𝕜 S →
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) y ∈ Algebra.adjoin 𝕜 S →
        ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (x * y) ∈ Algebra.adjoin 𝕜 S
case intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
refine Algebra.adjoin_induction hf ?_ ?_ ?_ ?_
no goals
case intro.intro.refine_1
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (x : C(X, 𝕜)), x ∈ S → ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) x ∈ Algebra.adjoin 𝕜 S
exact fun g hg => Algebra.subset_adjoin (hS g hg)
no goals
case intro.intro.refine_2
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (r : 𝕜),
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (↑(algebraMap 𝕜 C(X, 𝕜)) r) ∈ Algebra.adjoin 𝕜 S
exact fun c => Subalgebra.algebraMap_mem _ (starRingEnd 𝕜 c)
case intro.intro.refine_3
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f + g) ∈ Algebra.adjoin 𝕜 S
case intro.intro.refine_3
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (x y : C(X, 𝕜)),
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) x ∈ Algebra.adjoin 𝕜 S →
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) y ∈ Algebra.adjoin 𝕜 S →
        ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (x + y) ∈ Algebra.adjoin 𝕜 S
intro f g hf hg
case h.e'_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f + g) =
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f +
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g
case intro.intro.refine_3
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f + g) ∈ Algebra.adjoin 𝕜 S
convert Subalgebra.add_mem _ hf hg using 1
no goals
case h.e'_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f + g) =
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f +
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g
simp only [AlgEquiv.toAlgHom_eq_coe, map_add, RingHom.coe_coe]
case intro.intro.refine_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f * g) ∈ Algebra.adjoin 𝕜 S
case intro.intro.refine_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f : C(X, 𝕜)
hf : f ∈ Algebra.adjoin 𝕜 S
⊢ ∀ (x y : C(X, 𝕜)),
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) x ∈ Algebra.adjoin 𝕜 S →
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) y ∈ Algebra.adjoin 𝕜 S →
        ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (x * y) ∈ Algebra.adjoin 𝕜 S
intro f g hf hg
case h.e'_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f * g) =
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f *
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g
case intro.intro.refine_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f * g) ∈ Algebra.adjoin 𝕜 S
convert Subalgebra.mul_mem _ hf hg using 1
no goals
case h.e'_4
𝕜 : Type u_1
X : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
S : Set C(X, 𝕜)
hS : ∀ (f : C(X, 𝕜)), f ∈ S → ↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ S
f✝ : C(X, 𝕜)
hf✝ : f✝ ∈ Algebra.adjoin 𝕜 S
f g : C(X, 𝕜)
hf : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f ∈ Algebra.adjoin 𝕜 S
hg : ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g ∈ Algebra.adjoin 𝕜 S
⊢ ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) (f * g) =
    ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) f *
      ↑↑(AlgHom.compLeftContinuous ℝ ↑conjAe (_ : Continuous ↑conjCle)) g
simp only [AlgEquiv.toAlgHom_eq_coe, map_mul, RingHom.coe_coe]