[GOAL]
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
p : R[X]
⊢ Continuous fun x => eval x p
[PROOFSTEP]
continuity
[GOAL]
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
p : R[X]
X : Set R
⊢ Continuous ↑(toContinuousMap p)
[PROOFSTEP]
continuity
[GOAL]
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
p : R[X]
X : Set R
⊢ Continuous fun x => ↑x
[PROOFSTEP]
continuity
[GOAL]
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ↑(↑(aeval f) g) x = eval (↑f x) g
[PROOFSTEP]
refine' Polynomial.induction_on' g _ _
[GOAL]
case refine'_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (p q : R[X]),
    ↑(↑(aeval f) p) x = eval (↑f x) p →
      ↑(↑(aeval f) q) x = eval (↑f x) q → ↑(↑(aeval f) (p + q)) x = eval (↑f x) (p + q)
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine'_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
p q : R[X]
hp : ↑(↑(aeval f) p) x = eval (↑f x) p
hq : ↑(↑(aeval f) q) x = eval (↑f x) q
⊢ ↑(↑(aeval f) (p + q)) x = eval (↑f x) (p + q)
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case refine'_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (n : ℕ) (a : R), ↑(↑(aeval f) (↑(monomial n) a)) x = eval (↑f x) (↑(monomial n) a)
[PROOFSTEP]
intro n a
[GOAL]
case refine'_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
n : ℕ
a : R
⊢ ↑(↑(aeval f) (↑(monomial n) a)) x = eval (↑f x) (↑(monomial n) a)
[PROOFSTEP]
simp [Pi.pow_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
⊢ (fun p => toContinuousMap p) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a✝ : R
⊢ ↑((fun p => toContinuousMap p) 1) a✝ = ↑1 a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
x✝¹ x✝ : R[X]
⊢ OneHom.toFun { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
      (x✝¹ * x✝) =
    OneHom.toFun { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) } x✝¹ *
      OneHom.toFun { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) } x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
x✝¹ x✝ : R[X]
a✝ : R
⊢ ↑(OneHom.toFun { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
          (x✝¹ * x✝))
      a✝ =
    ↑(OneHom.toFun { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) } x✝¹ *
          OneHom.toFun { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) } x✝)
      a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x x_1 : R[X]),
                OneHom.toFun
                    { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                    (x * x_1) =
                  OneHom.toFun
                      { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) } x *
                    OneHom.toFun
                      { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                      x_1) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a✝ : R
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x x_1 : R[X]),
                    OneHom.toFun
                        { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                        (x * x_1) =
                      OneHom.toFun
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                          x_1) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
x✝¹ x✝ : R[X]
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x x_1 : R[X]),
                OneHom.toFun
                    { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                    (x * x_1) =
                  OneHom.toFun
                      { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) } x *
                    OneHom.toFun
                      { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                      x_1) })
      (x✝¹ + x✝) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x x_1 : R[X]),
                  OneHom.toFun
                      { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                      (x * x_1) =
                    OneHom.toFun
                        { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                        x_1) })
        x✝¹ +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x x_1 : R[X]),
                  OneHom.toFun
                      { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                      (x * x_1) =
                    OneHom.toFun
                        { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                        x_1) })
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
x✝¹ x✝ : R[X]
a✝ : R
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x x_1 : R[X]),
                    OneHom.toFun
                        { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                        (x * x_1) =
                      OneHom.toFun
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                          x_1) })
          (x✝¹ + x✝))
      a✝ =
    ↑(OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                          (x * x_1) =
                        OneHom.toFun
                            { toFun := fun p => toContinuousMap p,
                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun p => toContinuousMap p,
                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                            x_1) })
            x✝¹ +
          OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                          (x * x_1) =
                        OneHom.toFun
                            { toFun := fun p => toContinuousMap p,
                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun p => toContinuousMap p,
                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                            x_1) })
            x✝)
      a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
x✝ : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                          (x * x_1) =
                        OneHom.toFun
                            { toFun := fun p => toContinuousMap p,
                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun p => toContinuousMap p,
                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                            x_1) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x x_1 : R[X]),
                              OneHom.toFun
                                  { toFun := fun p => toContinuousMap p,
                                    map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                  (x * x_1) =
                                OneHom.toFun
                                    { toFun := fun p => toContinuousMap p,
                                      map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                    x *
                                  OneHom.toFun
                                    { toFun := fun p => toContinuousMap p,
                                      map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                    x_1) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x x_1 : R[X]),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p => toContinuousMap p,
                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x x_2 : R[X]),
                                OneHom.toFun
                                    { toFun := fun p => toContinuousMap p,
                                      map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                    (x * x_2) =
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMap p,
                                        map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                      x *
                                    OneHom.toFun
                                      { toFun := fun p => toContinuousMap p,
                                        map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                      x_2) })
                      (x + x_1) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p => toContinuousMap p,
                                map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_2 : R[X]),
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMap p,
                                        map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                      (x * x_2) =
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMap p,
                                          map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun p => toContinuousMap p,
                                          map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                        x_2) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p => toContinuousMap p,
                                map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_2 : R[X]),
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMap p,
                                        map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                      (x * x_2) =
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMap p,
                                          map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun p => toContinuousMap p,
                                          map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                        x_2) })
                        x_1) })
      (↑(algebraMap R R[X]) x✝) =
    ↑(algebraMap R C(R, R)) x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
x✝ a✝ : R
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  {
                    toOneHom :=
                      { toFun := fun p => toContinuousMap p, map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x x_1 : R[X]),
                          OneHom.toFun
                              { toFun := fun p => toContinuousMap p,
                                map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                              (x * x_1) =
                            OneHom.toFun
                                { toFun := fun p => toContinuousMap p,
                                  map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                x *
                              OneHom.toFun
                                { toFun := fun p => toContinuousMap p,
                                  map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                x_1) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p => toContinuousMap p,
                                map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_1 : R[X]),
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMap p,
                                        map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                      (x * x_1) =
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMap p,
                                          map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun p => toContinuousMap p,
                                          map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                        x_1) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p => toContinuousMap p,
                                  map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x x_2 : R[X]),
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMap p,
                                          map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                        (x * x_2) =
                                      OneHom.toFun
                                          { toFun := fun p => toContinuousMap p,
                                            map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                          x *
                                        OneHom.toFun
                                          { toFun := fun p => toContinuousMap p,
                                            map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                          x_2) })
                          (x + x_1) =
                        OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun p => toContinuousMap p,
                                    map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x x_2 : R[X]),
                                      OneHom.toFun
                                          { toFun := fun p => toContinuousMap p,
                                            map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                          (x * x_2) =
                                        OneHom.toFun
                                            { toFun := fun p => toContinuousMap p,
                                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                            x *
                                          OneHom.toFun
                                            { toFun := fun p => toContinuousMap p,
                                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                            x_2) })
                            x +
                          OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun p => toContinuousMap p,
                                    map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x x_2 : R[X]),
                                      OneHom.toFun
                                          { toFun := fun p => toContinuousMap p,
                                            map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                          (x * x_2) =
                                        OneHom.toFun
                                            { toFun := fun p => toContinuousMap p,
                                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                            x *
                                          OneHom.toFun
                                            { toFun := fun p => toContinuousMap p,
                                              map_one' := (_ : (fun p => toContinuousMap p) 1 = 1) }
                                            x_2) })
                            x_1) })
          (↑(algebraMap R R[X]) x✝))
      a✝ =
    ↑(↑(algebraMap R C(R, R)) x✝) a✝
[PROOFSTEP]
simp [Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
⊢ (fun p => toContinuousMapOn p X) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
a✝ : ↑X
⊢ ↑((fun p => toContinuousMapOn p X) 1) a✝ = ↑1 a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x✝¹ x✝ : R[X]
⊢ OneHom.toFun { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
      (x✝¹ * x✝) =
    OneHom.toFun { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
        x✝¹ *
      OneHom.toFun { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x✝¹ x✝ : R[X]
a✝ : ↑X
⊢ ↑(OneHom.toFun { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
          (x✝¹ * x✝))
      a✝ =
    ↑(OneHom.toFun { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
            x✝¹ *
          OneHom.toFun
            { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) } x✝)
      a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x x_1 : R[X]),
                OneHom.toFun
                    { toFun := fun p => toContinuousMapOn p X,
                      map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                    (x * x_1) =
                  OneHom.toFun
                      { toFun := fun p => toContinuousMapOn p X,
                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun p => toContinuousMapOn p X,
                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                      x_1) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
a✝ : ↑X
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x x_1 : R[X]),
                    OneHom.toFun
                        { toFun := fun p => toContinuousMapOn p X,
                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                        (x * x_1) =
                      OneHom.toFun
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                          x_1) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x✝¹ x✝ : R[X]
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x x_1 : R[X]),
                OneHom.toFun
                    { toFun := fun p => toContinuousMapOn p X,
                      map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                    (x * x_1) =
                  OneHom.toFun
                      { toFun := fun p => toContinuousMapOn p X,
                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun p => toContinuousMapOn p X,
                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                      x_1) })
      (x✝¹ + x✝) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x x_1 : R[X]),
                  OneHom.toFun
                      { toFun := fun p => toContinuousMapOn p X,
                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                      (x * x_1) =
                    OneHom.toFun
                        { toFun := fun p => toContinuousMapOn p X,
                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun p => toContinuousMapOn p X,
                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                        x_1) })
        x✝¹ +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x x_1 : R[X]),
                  OneHom.toFun
                      { toFun := fun p => toContinuousMapOn p X,
                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                      (x * x_1) =
                    OneHom.toFun
                        { toFun := fun p => toContinuousMapOn p X,
                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun p => toContinuousMapOn p X,
                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                        x_1) })
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x✝¹ x✝ : R[X]
a✝ : ↑X
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x x_1 : R[X]),
                    OneHom.toFun
                        { toFun := fun p => toContinuousMapOn p X,
                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                        (x * x_1) =
                      OneHom.toFun
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                          x_1) })
          (x✝¹ + x✝))
      a✝ =
    ↑(OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                          (x * x_1) =
                        OneHom.toFun
                            { toFun := fun p => toContinuousMapOn p X,
                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun p => toContinuousMapOn p X,
                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                            x_1) })
            x✝¹ +
          OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                          (x * x_1) =
                        OneHom.toFun
                            { toFun := fun p => toContinuousMapOn p X,
                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun p => toContinuousMapOn p X,
                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                            x_1) })
            x✝)
      a✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x✝ : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun p => toContinuousMapOn p X, map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                          (x * x_1) =
                        OneHom.toFun
                            { toFun := fun p => toContinuousMapOn p X,
                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun p => toContinuousMapOn p X,
                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                            x_1) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun p => toContinuousMapOn p X,
                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x x_1 : R[X]),
                              OneHom.toFun
                                  { toFun := fun p => toContinuousMapOn p X,
                                    map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                  (x * x_1) =
                                OneHom.toFun
                                    { toFun := fun p => toContinuousMapOn p X,
                                      map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                    x *
                                  OneHom.toFun
                                    { toFun := fun p => toContinuousMapOn p X,
                                      map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                    x_1) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x x_1 : R[X]),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun p => toContinuousMapOn p X,
                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x x_2 : R[X]),
                                OneHom.toFun
                                    { toFun := fun p => toContinuousMapOn p X,
                                      map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                    (x * x_2) =
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMapOn p X,
                                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                      x *
                                    OneHom.toFun
                                      { toFun := fun p => toContinuousMapOn p X,
                                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                      x_2) })
                      (x + x_1) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p => toContinuousMapOn p X,
                                map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_2 : R[X]),
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMapOn p X,
                                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                      (x * x_2) =
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMapOn p X,
                                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun p => toContinuousMapOn p X,
                                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                        x_2) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p => toContinuousMapOn p X,
                                map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_2 : R[X]),
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMapOn p X,
                                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                      (x * x_2) =
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMapOn p X,
                                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun p => toContinuousMapOn p X,
                                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                        x_2) })
                        x_1) })
      (↑(algebraMap R R[X]) x✝) =
    ↑(algebraMap R C(↑X, R)) x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x✝ : R
a✝ : ↑X
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  {
                    toOneHom :=
                      { toFun := fun p => toContinuousMapOn p X,
                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x x_1 : R[X]),
                          OneHom.toFun
                              { toFun := fun p => toContinuousMapOn p X,
                                map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                              (x * x_1) =
                            OneHom.toFun
                                { toFun := fun p => toContinuousMapOn p X,
                                  map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                x *
                              OneHom.toFun
                                { toFun := fun p => toContinuousMapOn p X,
                                  map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                x_1) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun p => toContinuousMapOn p X,
                                map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_1 : R[X]),
                                  OneHom.toFun
                                      { toFun := fun p => toContinuousMapOn p X,
                                        map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                      (x * x_1) =
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMapOn p X,
                                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun p => toContinuousMapOn p X,
                                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                        x_1) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x x_1 : R[X]),
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun p => toContinuousMapOn p X,
                                  map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x x_2 : R[X]),
                                    OneHom.toFun
                                        { toFun := fun p => toContinuousMapOn p X,
                                          map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                        (x * x_2) =
                                      OneHom.toFun
                                          { toFun := fun p => toContinuousMapOn p X,
                                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                          x *
                                        OneHom.toFun
                                          { toFun := fun p => toContinuousMapOn p X,
                                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                          x_2) })
                          (x + x_1) =
                        OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun p => toContinuousMapOn p X,
                                    map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x x_2 : R[X]),
                                      OneHom.toFun
                                          { toFun := fun p => toContinuousMapOn p X,
                                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                          (x * x_2) =
                                        OneHom.toFun
                                            { toFun := fun p => toContinuousMapOn p X,
                                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                            x *
                                          OneHom.toFun
                                            { toFun := fun p => toContinuousMapOn p X,
                                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                            x_2) })
                            x +
                          OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun p => toContinuousMapOn p X,
                                    map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x x_2 : R[X]),
                                      OneHom.toFun
                                          { toFun := fun p => toContinuousMapOn p X,
                                            map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                          (x * x_2) =
                                        OneHom.toFun
                                            { toFun := fun p => toContinuousMapOn p X,
                                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                            x *
                                          OneHom.toFun
                                            { toFun := fun p => toContinuousMapOn p X,
                                              map_one' := (_ : (fun p => toContinuousMapOn p X) 1 = 1) }
                                            x_2) })
                            x_1) })
          (↑(algebraMap R R[X]) x✝))
      a✝ =
    ↑(↑(algebraMap R C(↑X, R)) x✝) a✝
[PROOFSTEP]
simp [Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
⊢ ↑(polynomialFunctions X) = Set.range ↑(toContinuousMapOnAlgHom X)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x✝ : C(↑X, R)
⊢ x✝ ∈ ↑(polynomialFunctions X) ↔ x✝ ∈ Set.range ↑(toContinuousMapOnAlgHom X)
[PROOFSTEP]
simp [polynomialFunctions]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑(polynomialFunctions X) ∧ f x ≠ f y
[PROOFSTEP]
refine' ⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, _⟩⟩
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ (fun f => ↑f) (↑↑(toContinuousMapOnAlgHom X) Polynomial.X) x ≠
    (fun f => ↑f) (↑↑(toContinuousMapOnAlgHom X) Polynomial.X) y
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X
[PROOFSTEP]
simp only [Polynomial.eval_X]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬↑x = ↑y
[PROOFSTEP]
exact fun h' => h (Subtype.ext h')
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
⊢ Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (polynomialFunctions I) =
    polynomialFunctions (Set.Icc a b)
[PROOFSTEP]
ext f
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈
      Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
        (polynomialFunctions I) ↔
    f ∈ polynomialFunctions (Set.Icc a b)
[PROOFSTEP]
fconstructor
[GOAL]
case h.mp
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈
      Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
        (polynomialFunctions I) →
    f ∈ polynomialFunctions (Set.Icc a b)
[PROOFSTEP]
rintro ⟨p, ⟨-, w⟩⟩
[GOAL]
case h.mp.intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
⊢ f ∈ polynomialFunctions (Set.Icc a b)
[PROOFSTEP]
rw [FunLike.ext_iff] at w
[GOAL]
case h.mp.intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w :
  ∀ (x : ↑I),
    ↑(↑↑(toContinuousMapOnAlgHom I) p) x =
      ↑(↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f) x
⊢ f ∈ polynomialFunctions (Set.Icc a b)
[PROOFSTEP]
dsimp at w
[GOAL]
case h.mp.intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
⊢ f ∈ polynomialFunctions (Set.Icc a b)
[PROOFSTEP]
let q := p.comp ((b - a)⁻¹ • Polynomial.X + Polynomial.C (-a * (b - a)⁻¹))
[GOAL]
case h.mp.intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
⊢ f ∈ polynomialFunctions (Set.Icc a b)
[PROOFSTEP]
refine' ⟨q, ⟨_, _⟩⟩
[GOAL]
case h.mp.intro.intro.refine'_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
⊢ q ∈ ↑⊤.toSubsemiring
[PROOFSTEP]
simp
[GOAL]
case h.mp.intro.intro.refine'_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
⊢ ↑↑(toContinuousMapOnAlgHom (Set.Icc a b)) q = f
[PROOFSTEP]
ext x
[GOAL]
case h.mp.intro.intro.refine'_2.h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ ↑(↑↑(toContinuousMapOnAlgHom (Set.Icc a b)) q) x = ↑f x
[PROOFSTEP]
simp only [neg_mul, RingHom.map_neg, RingHom.map_mul, AlgHom.coe_toRingHom, Polynomial.eval_X, Polynomial.eval_neg,
  Polynomial.eval_C, Polynomial.eval_smul, smul_eq_mul, Polynomial.eval_mul, Polynomial.eval_add,
  Polynomial.coe_aeval_eq_eval, Polynomial.eval_comp, Polynomial.toContinuousMapOnAlgHom_apply,
  Polynomial.toContinuousMapOn_apply, Polynomial.toContinuousMap_apply]
[GOAL]
case h.mp.intro.intro.refine'_2.h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ Polynomial.eval ((b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹)) p = ↑f x
[PROOFSTEP]
convert w ⟨_, _⟩
[GOAL]
case h.e'_3.h.e'_6
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ x =
    ↑(Homeomorph.symm (iccHomeoI a b h))
      { val := (b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹), property := ?h.mp.intro.intro.refine'_2.h.convert_2 }
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_6.a
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ ↑x =
    ↑(↑(Homeomorph.symm (iccHomeoI a b h))
        { val := (b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹), property := ?h.mp.intro.intro.refine'_2.h.convert_2 })
[PROOFSTEP]
simp only [iccHomeoI_symm_apply_coe, Subtype.coe_mk]
[GOAL]
case h.e'_3.h.e'_6.a
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ ↑x = (b - a) * ((b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹)) + a
[PROOFSTEP]
replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm
[GOAL]
case h.e'_3.h.e'_6.a
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h✝ : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h✝)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h✝)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
h : b - a ≠ 0
⊢ ↑x = (b - a) * ((b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹)) + a
[PROOFSTEP]
simp only [mul_add]
[GOAL]
case h.e'_3.h.e'_6.a
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h✝ : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h✝)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h✝)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
h : b - a ≠ 0
⊢ ↑x = (b - a) * ((b - a)⁻¹ * ↑x) + (b - a) * -(a * (b - a)⁻¹) + a
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3.h.e'_6.a
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h✝ : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h✝)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h✝)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
h : b - a ≠ 0
⊢ ↑x * (b - a) = (b - a) * ↑x + -((b - a) * a) + a * (b - a)
[PROOFSTEP]
ring
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ (b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹) ∈ I
[PROOFSTEP]
change _ + _ ∈ I
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ (b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹) ∈ I
[PROOFSTEP]
rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ (↑x - a) * (b - a)⁻¹ ∈ I
[PROOFSTEP]
have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
⊢ (↑x - a) * (b - a)⁻¹ ∈ I
[PROOFSTEP]
have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
w₂ : 0 ≤ ↑x - a
⊢ (↑x - a) * (b - a)⁻¹ ∈ I
[PROOFSTEP]
have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
w₂ : 0 ≤ ↑x - a
w₃ : ↑x - a ≤ b - a
⊢ (↑x - a) * (b - a)⁻¹ ∈ I
[PROOFSTEP]
fconstructor
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2.left
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
w₂ : 0 ≤ ↑x - a
w₃ : ↑x - a ≤ b - a
⊢ 0 ≤ (↑x - a) * (b - a)⁻¹
[PROOFSTEP]
exact mul_nonneg w₂ (le_of_lt w₁)
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2.right
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
w₂ : 0 ≤ ↑x - a
w₃ : ↑x - a ≤ b - a
⊢ (↑x - a) * (b - a)⁻¹ ≤ 1
[PROOFSTEP]
rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]
[GOAL]
case h.mp.intro.intro.refine'_2.h.convert_2.right
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w✝ :
  ↑↑(toContinuousMapOnAlgHom I) p =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))) f
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = ↑f (↑(Homeomorph.symm (iccHomeoI a b h)) x)
q : ℝ[X] := Polynomial.comp p ((b - a)⁻¹ • X + ↑Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
w₂ : 0 ≤ ↑x - a
w₃ : ↑x - a ≤ b - a
⊢ ↑x - a ≤ b - a
[PROOFSTEP]
exact w₃
[GOAL]
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ polynomialFunctions (Set.Icc a b) →
    f ∈
      Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
        (polynomialFunctions I)
[PROOFSTEP]
rintro ⟨p, ⟨-, rfl⟩⟩
[GOAL]
case h.mpr.intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
p : ℝ[X]
⊢ ↑↑(toContinuousMapOnAlgHom (Set.Icc a b)) p ∈
    Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (polynomialFunctions I)
[PROOFSTEP]
let q := p.comp ((b - a) • Polynomial.X + Polynomial.C a)
[GOAL]
case h.mpr.intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := Polynomial.comp p ((b - a) • X + ↑Polynomial.C a)
⊢ ↑↑(toContinuousMapOnAlgHom (Set.Icc a b)) p ∈
    Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (polynomialFunctions I)
[PROOFSTEP]
refine' ⟨q, ⟨_, _⟩⟩
[GOAL]
case h.mpr.intro.intro.refine'_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := Polynomial.comp p ((b - a) • X + ↑Polynomial.C a)
⊢ q ∈ ↑⊤.toSubsemiring
[PROOFSTEP]
simp
[GOAL]
case h.mpr.intro.intro.refine'_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := Polynomial.comp p ((b - a) • X + ↑Polynomial.C a)
⊢ ↑↑(toContinuousMapOnAlgHom I) q =
    ↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (↑↑(toContinuousMapOnAlgHom (Set.Icc a b)) p)
[PROOFSTEP]
ext x
[GOAL]
case h.mpr.intro.intro.refine'_2.h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := Polynomial.comp p ((b - a) • X + ↑Polynomial.C a)
x : ↑I
⊢ ↑(↑↑(toContinuousMapOnAlgHom I) q) x =
    ↑(↑↑(compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
          (↑↑(toContinuousMapOnAlgHom (Set.Icc a b)) p))
      x
[PROOFSTEP]
simp [mul_comm]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set R
⊢ polynomialFunctions s = Algebra.adjoin R {↑(toContinuousMapOnAlgHom s) X}
[PROOFSTEP]
refine le_antisymm ?_ (Algebra.adjoin_le fun _ h => ⟨X, trivial, (Set.mem_singleton_iff.1 h).symm⟩)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set R
⊢ polynomialFunctions s ≤ Algebra.adjoin R {↑(toContinuousMapOnAlgHom s) X}
[PROOFSTEP]
rintro - ⟨p, -, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set R
p : R[X]
⊢ ↑↑(toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {↑(toContinuousMapOnAlgHom s) X}
[PROOFSTEP]
rw [AlgHom.coe_toRingHom]
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set R
p : R[X]
⊢ ↑(toContinuousMapOnAlgHom s) p ∈ Algebra.adjoin R {↑(toContinuousMapOnAlgHom s) X}
[PROOFSTEP]
refine p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_
[GOAL]
case intro.intro.refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ ↑(toContinuousMapOnAlgHom s) (↑Polynomial.C r) ∈ Algebra.adjoin R {↑(toContinuousMapOnAlgHom s) X}
[PROOFSTEP]
rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]
[GOAL]
case intro.intro.refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ ↑(algebraMap R C(↑s, R)) r ∈ Algebra.adjoin R {↑(toContinuousMapOnAlgHom s) X}
[PROOFSTEP]
exact Subalgebra.algebraMap_mem _ r
[GOAL]
case intro.intro.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring 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}
[PROOFSTEP]
rw [map_add]
[GOAL]
case intro.intro.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring 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}
[PROOFSTEP]
exact add_mem hf hg
[GOAL]
case intro.intro.refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring 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}
[PROOFSTEP]
rw [pow_succ', ← mul_assoc, map_mul]
[GOAL]
case intro.intro.refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring 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}
[PROOFSTEP]
exact mul_mem hn (Algebra.subset_adjoin <| Set.mem_singleton _)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : ↑φ (↑(toContinuousMapOnAlgHom s) X) = ↑ψ (↑(toContinuousMapOnAlgHom s) X)
⊢ polynomialFunctions s ≤ AlgHom.equalizer φ ψ
[PROOFSTEP]
rw [polynomialFunctions.eq_adjoin_X s]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : ↑φ (↑(toContinuousMapOnAlgHom s) X) = ↑ψ (↑(toContinuousMapOnAlgHom s) X)
⊢ Algebra.adjoin R {↑(toContinuousMapOnAlgHom s) X} ≤ AlgHom.equalizer φ ψ
[PROOFSTEP]
exact φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSemiring R
inst✝¹ : StarRing R
inst✝ : ContinuousStar R
s : Set R
⊢ Subalgebra.starClosure (polynomialFunctions s) = adjoin R {↑(toContinuousMapOnAlgHom s) X}
[PROOFSTEP]
rw [polynomialFunctions.eq_adjoin_X s, adjoin_eq_starClosure_adjoin]
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
A : Type u_2
inst✝⁴ : StarRing R
inst✝³ : ContinuousStar R
inst✝² : Semiring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →⋆ₐ[R] A
h : ↑φ (↑(toContinuousMapOnAlgHom s) X) = ↑ψ (↑(toContinuousMapOnAlgHom s) X)
⊢ Subalgebra.starClosure (polynomialFunctions s) ≤ StarAlgHom.equalizer φ ψ
[PROOFSTEP]
rw [polynomialFunctions.starClosure_eq_adjoin_X s]
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSemiring R
A : Type u_2
inst✝⁴ : StarRing R
inst✝³ : ContinuousStar R
inst✝² : Semiring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →⋆ₐ[R] A
h : ↑φ (↑(toContinuousMapOnAlgHom s) X) = ↑ψ (↑(toContinuousMapOnAlgHom s) X)
⊢ adjoin R {↑(toContinuousMapOnAlgHom s) X} ≤ StarAlgHom.equalizer φ ψ
[PROOFSTEP]
exact StarAlgHom.adjoin_le_equalizer φ ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h


[GOAL]
X : CompHaus
inst✝ : Projective X
⊢ ExtremallyDisconnected ↑X.toTop
[PROOFSTEP]
apply CompactT2.Projective.extremallyDisconnected
[GOAL]
case h
X : CompHaus
inst✝ : Projective X
⊢ CompactT2.Projective ↑X.toTop
[PROOFSTEP]
intro A B _ _ _ _ _ _ f g hf hg hsurj
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : CompactSpace (TopCat.of A) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
⊢ CompactSpace ↑(TopCat.of A)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this : CompactSpace ↑(TopCat.of A)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : T2Space (TopCat.of A) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this : CompactSpace ↑(TopCat.of A)
⊢ T2Space ↑(TopCat.of A)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝ : CompactSpace ↑(TopCat.of A)
this : T2Space ↑(TopCat.of A)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : CompactSpace (TopCat.of B) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝ : CompactSpace ↑(TopCat.of A)
this : T2Space ↑(TopCat.of A)
⊢ CompactSpace ↑(TopCat.of B)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝¹ : CompactSpace ↑(TopCat.of A)
this✝ : T2Space ↑(TopCat.of A)
this : CompactSpace ↑(TopCat.of B)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : T2Space (TopCat.of B) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝¹ : CompactSpace ↑(TopCat.of A)
this✝ : T2Space ↑(TopCat.of A)
this : CompactSpace ↑(TopCat.of B)
⊢ T2Space ↑(TopCat.of B)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let A' : CompHaus := ⟨TopCat.of A⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let B' : CompHaus := ⟨TopCat.of B⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let f' : X ⟶ B' := ⟨f, hf⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let g' : A' ⟶ B' := ⟨g, hg⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : Epi g' := by
  rw [CompHaus.epi_iff_surjective]
  assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
⊢ Epi g'
[PROOFSTEP]
rw [CompHaus.epi_iff_surjective]
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
⊢ Function.Surjective ↑g'
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
obtain ⟨h, hh⟩ := Projective.factors f' g'
[GOAL]
case h.intro
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
refine ⟨h, h.2, ?_⟩
[GOAL]
case h.intro
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
⊢ g ∘ ↑h = f
[PROOFSTEP]
ext t
[GOAL]
case h.intro.h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
t : ↑X.toTop
⊢ (g ∘ ↑h) t = f t
[PROOFSTEP]
apply_fun (fun e => e t) at hh
[GOAL]
case h.intro.h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
t : ↑X.toTop
hh : ↑(h ≫ g') t = ↑f' t
⊢ (g ∘ ↑h) t = f t
[PROOFSTEP]
exact hh