-- Mathlib/Topology/ContinuousMap/Weierstrass.lean
theorem polynomialFunctions_closure_eq_top (a b : ℝ) :
    (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inr
a b : ℝ
h : b ≤ a
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
subsingleton [(Set.subsingleton_Icc_of_ge h).coe_sort]

Result:
no goals

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : Subalgebra.comap W (polynomialFunctions I).topologicalClosure = Subalgebra.comap W ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
simp only [Algebra.comap_top] at p

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : Subalgebra.comap W (polynomialFunctions I).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
let W : C(Set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) :=
  compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : Subalgebra.comap W (polynomialFunctions I).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (Subalgebra.comap W (polynomialFunctions I)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions I).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
apply_fun fun s => s.comap W at p

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : Subalgebra.comap W (polynomialFunctions I).topologicalClosure = Subalgebra.comap W ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
exact p

Result:
no goals

Proof state:
a b : ℝ
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
rcases lt_or_le a b with h | h

Result:
case inl
a b : ℝ
h : a < b
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

case inr
a b : ℝ
h : b ≤ a
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (Subalgebra.comap W (polynomialFunctions I)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := (iccHomeoI a b h).arrowCongr (.refl _)

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Proof state:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Tactic:
have p := polynomialFunctions_closure_eq_top'

Result:
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) := compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := (iccHomeoI a b h).arrowCongr (Homeomorph.refl ℝ)
w : ⇑W = ⇑W'
p : (polynomialFunctions I).topologicalClosure = ⊤
⊢ (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤