case h
R : Type ?u.106978
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)
R : Type ?u.106978
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)
ext f
case h.mp
R : Type ?u.106978
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)

case h.mpr
R : Type ?u.106978
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)
case h
R : Type ?u.106978
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)
fconstructor
case h.mp.intro.intro
R : Type ?u.106978
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)
case h.mp
R : Type ?u.106978
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)
rintro ⟨p, ⟨-, w⟩⟩
case h.mp.intro.intro
R : Type ?u.106978
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)
case h.mp.intro.intro
R : Type ?u.106978
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)
rw [FunLike.ext_iff] at w
case h.mp.intro.intro
R : Type ?u.106978
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)
case h.mp.intro.intro
R : Type ?u.106978
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)
dsimp at w
case h.mp.intro.intro
R : Type ?u.106978
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)
case h.mp.intro.intro
R : Type ?u.106978
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)
let q := p.comp ((b - a)⁻¹ • Polynomial.X + Polynomial.C (-a * (b - a)⁻¹))
case h.mp.intro.intro.refine'_1
R : Type ?u.106978
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

case h.mp.intro.intro.refine'_2
R : Type ?u.106978
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
case h.mp.intro.intro
R : Type ?u.106978
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)
refine' ⟨q, ⟨_, _⟩⟩
no goals
case h.mp.intro.intro.refine'_1
R : Type ?u.106978
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
simp
case h.mp.intro.intro.refine'_2.h
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2
R : Type ?u.106978
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
ext x
case h.mp.intro.intro.refine'_2.h
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h
R : Type ?u.106978
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
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]
case h.e'_3.h.e'_6
R : Type ?u.106978
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 }

case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h
R : Type ?u.106978
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
convert w ⟨_, _⟩
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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 })
case h.e'_3.h.e'_6
R : Type ?u.106978
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 }
ext
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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 })
simp only [iccHomeoI_symm_apply_coe, Subtype.coe_mk]
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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
replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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
simp only [mul_add]
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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)
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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
field_simp
no goals
case h.e'_3.h.e'_6.a
R : Type ?u.106978
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)
ring
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
change _ + _ ∈ I
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a
case h.mp.intro.intro.refine'_2.h.convert_2.left
R : Type ?u.106978
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)⁻¹

case h.mp.intro.intro.refine'_2.h.convert_2.right
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h.convert_2
R : Type ?u.106978
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
fconstructor
no goals
case h.mp.intro.intro.refine'_2.h.convert_2.left
R : Type ?u.106978
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)⁻¹
exact mul_nonneg w₂ (le_of_lt w₁)
case h.mp.intro.intro.refine'_2.h.convert_2.right
R : Type ?u.106978
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
case h.mp.intro.intro.refine'_2.h.convert_2.right
R : Type ?u.106978
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
rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]
no goals
case h.mp.intro.intro.refine'_2.h.convert_2.right
R : Type ?u.106978
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
exact w₃
case h.mpr.intro.intro
R : Type ?u.106978
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)
case h.mpr
R : Type ?u.106978
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)
rintro ⟨p, ⟨-, rfl⟩⟩
case h.mpr.intro.intro
R : Type ?u.106978
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)
case h.mpr.intro.intro
R : Type ?u.106978
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)
let q := p.comp ((b - a) • Polynomial.X + Polynomial.C a)
case h.mpr.intro.intro.refine'_1
R : Type ?u.106978
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

case h.mpr.intro.intro.refine'_2
R : Type ?u.106978
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)
case h.mpr.intro.intro
R : Type ?u.106978
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)
refine' ⟨q, ⟨_, _⟩⟩
no goals
case h.mpr.intro.intro.refine'_1
R : Type ?u.106978
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
simp
case h.mpr.intro.intro.refine'_2.h
R : Type ?u.106978
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
case h.mpr.intro.intro.refine'_2
R : Type ?u.106978
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)
ext x
no goals
case h.mpr.intro.intro.refine'_2.h
R : Type ?u.106978
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
simp [mul_comm]