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

case neg
a b : ℝ
h : ¬a < b
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
a b : ℝ
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
by_cases h : a < b
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
let W : C(Set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) :=
  compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm.toContinuousMap
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := compRightHomeomorph ℝ (iccHomeoI a b h).symm
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions I) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
have p := polynomialFunctions_closure_eq_top'
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = Subalgebra.comap W ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions I) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
apply_fun fun s => s.comap W at p
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p :
  Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (Subalgebra.topologicalClosure (polynomialFunctions I)) =
    ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = Subalgebra.comap W ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
simp only [Algebra.comap_top] at p
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (Subalgebra.comap W (polynomialFunctions I)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p :
  Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (Subalgebra.topologicalClosure (polynomialFunctions I)) =
    ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (Subalgebra.comap W (polynomialFunctions I)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p
no goals
case pos
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
exact p
case neg
a b : ℝ
h : ¬a < b
this : Subsingleton ↑(Set.Icc a b)
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
case neg
a b : ℝ
h : ¬a < b
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
haveI : Subsingleton (Set.Icc a b) :=
  ⟨fun x y =>
    le_antisymm ((x.2.2.trans (not_lt.mp h)).trans y.2.1)
      ((y.2.2.trans (not_lt.mp h)).trans x.2.1)⟩
no goals
case neg
a b : ℝ
h : ¬a < b
this : Subsingleton ↑(Set.Icc a b)
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
apply Subsingleton.elim