-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem polynomialFunctions.eq_adjoin_X (s : Set R) :
    polynomialFunctions s = Algebra.adjoin R {toContinuousMapOnAlgHom s X}

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
⊢ ↑(toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
rw [AlgHom.coe_toRingHom]

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
⊢ (toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Proof state:
case intro.intro.refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) * (toContinuousMapOnAlgHom s) X ∈
    Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
exact mul_mem hn (Algebra.subset_adjoin <| Set.mem_singleton _)

Result:
no goals

Proof state:
case intro.intro.refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]

Result:
case intro.intro.refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (algebraMap R C(↑s, R)) r ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Proof state:
case intro.intro.refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
rw [pow_succ, ← mul_assoc, map_mul]

Result:
case intro.intro.refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) * (toContinuousMapOnAlgHom s) X ∈
    Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf : (toContinuousMapOnAlgHom s) f ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
hg : (toContinuousMapOnAlgHom s) g ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) (f + g) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
rw [map_add]

Result:
case intro.intro.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf : (toContinuousMapOnAlgHom s) f ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
hg : (toContinuousMapOnAlgHom s) g ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) f + (toContinuousMapOnAlgHom s) g ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf : (toContinuousMapOnAlgHom s) f ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
hg : (toContinuousMapOnAlgHom s) g ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) f + (toContinuousMapOnAlgHom s) g ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
exact add_mem hf hg

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
⊢ (toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
refine p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_

Result:
case intro.intro.refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

case intro.intro.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf : (toContinuousMapOnAlgHom s) f ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
hg : (toContinuousMapOnAlgHom s) g ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) (f + g) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

case intro.intro.refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn : (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ n) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}
⊢ (toContinuousMapOnAlgHom s) (Polynomial.C r * X ^ (n + 1)) ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Proof state:
case intro.intro.refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ (algebraMap R C(↑s, R)) r ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
exact Subalgebra.algebraMap_mem _ r

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
⊢ polynomialFunctions s = Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
refine le_antisymm ?_
  (Algebra.adjoin_le fun _ h => ⟨X, trivial, (Set.mem_singleton_iff.1 h).symm⟩)

Result:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
⊢ polynomialFunctions s ≤ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Proof state:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
⊢ polynomialFunctions s ≤ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
rintro - ⟨p, -, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
p : R[X]
⊢ ↑(toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X}