-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem polynomialFunctions.comap_compRightAlgHom_iccHomeoI (a b : ℝ) (h : a < b) :
    (polynomialFunctions I).comap (compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm) =
      polynomialFunctions (Set.Icc a b)

Proof state:
case h.mp.intro.intro.refine_2.h.convert_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((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

Tactic:
fconstructor

Result:
case h.mp.intro.intro.refine_2.h.convert_2.left
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((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
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((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

Proof state:
case h
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) ↔
    f ∈ polynomialFunctions (Set.Icc a b)

Tactic:
fconstructor

Result:
case h.mp
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) →
    f ∈ polynomialFunctions (Set.Icc a b)

case h.mpr
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ polynomialFunctions (Set.Icc a b) →
    f ∈ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I)

Proof state:
a b : ℝ
h : a < b
⊢ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) =
    polynomialFunctions (Set.Icc a b)

Tactic:
ext f

Result:
case h
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) ↔
    f ∈ polynomialFunctions (Set.Icc a b)

Proof state:
case h.mp.intro.intro.refine_2.h.convert_2.left
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((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)⁻¹

Tactic:
exact mul_nonneg w₂ (le_of_lt w₁)

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.a
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ ↑x = (b - a) * ((b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹)) + a

Tactic:
replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm

Result:
case h.e'_3.h.e'_6.a
a b : ℝ
h✝ : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h✝).symm x)
q : ℝ[X] := p.comp ((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

Proof state:
case h.mp.intro.intro.refine_2.h.convert_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
⊢ (↑x - a) * (b - a)⁻¹ ∈ I

Tactic:
have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1

Result:
case h.mp.intro.intro.refine_2.h.convert_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((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

Proof state:
case h.mp.intro.intro.refine_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
⊢ ↑(toContinuousMapOnAlgHom (Set.Icc a b)) q = f

Tactic:
ext x

Result:
case h.mp.intro.intro.refine_2.h
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ (↑(toContinuousMapOnAlgHom (Set.Icc a b)) q) x = f x

Proof state:
case h.mp.intro.intro
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
⊢ f ∈ polynomialFunctions (Set.Icc a b)

Tactic:
let q := p.comp ((b - a)⁻¹ • Polynomial.X + Polynomial.C (-a * (b - a)⁻¹))

Result:
case h.mp.intro.intro
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
⊢ f ∈ polynomialFunctions (Set.Icc a b)

Proof state:
case h.mp.intro.intro
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), (↑(toContinuousMapOnAlgHom I) p) x = (↑(compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) f) x
⊢ f ∈ polynomialFunctions (Set.Icc a b)

Tactic:
dsimp at w

Result:
case h.mp.intro.intro
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
⊢ f ∈ polynomialFunctions (Set.Icc a b)

Proof state:
case h.mpr.intro.intro.refine_1
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := p.comp ((b - a) • X + Polynomial.C a)
⊢ q ∈ ↑⊤.toSubsemiring

Tactic:
simp

Result:
no goals

Proof state:
case h.mpr.intro.intro
a b : ℝ
h : a < b
p : ℝ[X]
⊢ ↑(toContinuousMapOnAlgHom (Set.Icc a b)) p ∈
    Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I)

Tactic:
let q := p.comp ((b - a) • Polynomial.X + Polynomial.C a)

Result:
case h.mpr.intro.intro
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := p.comp ((b - a) • X + Polynomial.C a)
⊢ ↑(toContinuousMapOnAlgHom (Set.Icc a b)) p ∈
    Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I)

Proof state:
case h.mp
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) →
    f ∈ polynomialFunctions (Set.Icc a b)

Tactic:
rintro ⟨p, ⟨-, w⟩⟩

Result:
case h.mp.intro.intro
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ↑(toContinuousMapOnAlgHom I) p = ↑(compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) f
⊢ f ∈ polynomialFunctions (Set.Icc a b)

Proof state:
case h.mp.intro.intro.refine_2.h.convert_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ (↑x - a) * (b - a)⁻¹ ∈ I

Tactic:
have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)

Result:
case h.mp.intro.intro.refine_2.h.convert_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
w₁ : 0 < (b - a)⁻¹
⊢ (↑x - a) * (b - a)⁻¹ ∈ I