awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x a : R
⊢ Eq (α := R) ((toContinuousMap ((algebraMap R R[X] : (a : R) → R[X]) x) : (a : R) → R) a : R)
    ((((algebraMap R C(R, R) : (a : R) → C(R, R)) x : C(R, R)) : (a : R) → R) a : R)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
h :
  ∀ (a : (↑X : Type u_1)),
    Eq (α := R) ((toContinuousMapOn 1 X : (a : (↑X : Type u_1)) → R) a : R) ((1 : (a : (↑X : Type u_1)) → R) a : R)
⊢ Eq (α := C((↑X : Type u_1), R)) (toContinuousMapOn 1 X) 1

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
a : (↑X : Type u_1)
⊢ Eq (α := R) ((toContinuousMapOn 1 X : (a : (↑X : Type u_1)) → R) a : R) ((1 : (a : (↑X : Type u_1)) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x x_1 : R[X]
h :
  ∀ (a : (↑X : Type u_1)),
    Eq (α := R) (((x * x_1).toContinuousMapOn X : (a : (↑X : Type u_1)) → R) a : R)
      ((HMul.hMul (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X) :
            (a : (↑X : Type u_1)) → R)
          a :
        R)
⊢ (x * x_1).toContinuousMapOn X =
    HMul.hMul (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X)

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x x_1 : R[X]
a : (↑X : Type u_1)
⊢ Eq (α := R) (((x * x_1).toContinuousMapOn X : (a : (↑X : Type u_1)) → R) a : R)
    ((HMul.hMul (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X) :
          (a : (↑X : Type u_1)) → R)
        a :
      R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
h :
  ∀ (a : (↑X : Type u_1)),
    Eq (α := R) ((toContinuousMapOn 0 X : (a : (↑X : Type u_1)) → R) a : R) ((0 : (a : (↑X : Type u_1)) → R) a : R)
⊢ Eq (α := C((↑X : Type u_1), R)) (toContinuousMapOn 0 X) 0

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
a : (↑X : Type u_1)
⊢ Eq (α := R) ((toContinuousMapOn 0 X : (a : (↑X : Type u_1)) → R) a : R) ((0 : (a : (↑X : Type u_1)) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x x_1 : R[X]
h :
  ∀ (a : (↑X : Type u_1)),
    Eq (α := R) (((x + x_1).toContinuousMapOn X : (a : (↑X : Type u_1)) → R) a : R)
      ((HAdd.hAdd (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X) :
            (a : (↑X : Type u_1)) → R)
          a :
        R)
⊢ (x + x_1).toContinuousMapOn X =
    HAdd.hAdd (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X)

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x x_1 : R[X]
a : (↑X : Type u_1)
⊢ Eq (α := R) (((x + x_1).toContinuousMapOn X : (a : (↑X : Type u_1)) → R) a : R)
    ((HAdd.hAdd (α := C((↑X : Type u_1), R)) (x.toContinuousMapOn X) (x_1.toContinuousMapOn X) :
          (a : (↑X : Type u_1)) → R)
        a :
      R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x : R
h :
  ∀ (a : (↑X : Type u_1)),
    Eq (α := R) ((toContinuousMapOn ((algebraMap R R[X] : (a : R) → R[X]) x) X : (a : (↑X : Type u_1)) → R) a : R)
      ((((algebraMap R C((↑X : Type u_1), R) : (a : R) → C((↑X : Type u_1), R)) x : C((↑X : Type u_1), R)) :
            (a : (↑X : Type u_1)) → R)
          a :
        R)
⊢ Eq (α := C((↑X : Type u_1), R)) (toContinuousMapOn ((algebraMap R R[X] : (a : R) → R[X]) x) X)
    ((algebraMap R C((↑X : Type u_1), R) : (a : R) → C((↑X : Type u_1), R)) x)

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x : R
a : (↑X : Type u_1)
⊢ Eq (α := R) ((toContinuousMapOn ((algebraMap R R[X] : (a : R) → R[X]) x) X : (a : (↑X : Type u_1)) → R) a : R)
    ((((algebraMap R C((↑X : Type u_1), R) : (a : R) → C((↑X : Type u_1), R)) x : C((↑X : Type u_1), R)) :
          (a : (↑X : Type u_1)) → R)
        a :
      R)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
h :
  ∀ (x : C((↑X : Type u_1), R)),
    x ∈ (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)) ↔
      Membership.mem (γ := Set C((↑X : Type u_1), R))
        (Set.range (ι := R[X]) (⇑(toContinuousMapOnAlgHom X) : (a : R[X]) → C((↑X : Type u_1), R))) x
⊢ (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)) =
    Set.range (ι := R[X]) (⇑(toContinuousMapOnAlgHom X) : (a : R[X]) → C((↑X : Type u_1), R))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x : C((↑X : Type u_1), R)
⊢ x ∈ (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)) ↔
    Membership.mem (γ := Set C((↑X : Type u_1), R))
      (Set.range (ι := R[X]) (⇑(toContinuousMapOnAlgHom X) : (a : R[X]) → C((↑X : Type u_1), R))) x

Tactic:
simp [polynomialFunctions]

Premises used: polynomialFunctions
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x y : (↑X : Type u_1)
h : x ≠ y
⊢ ∃ (f : (↑X : Type u_1) → R),
    Membership.mem (γ := Set ((↑X : Type u_1) → R))
        ((fun (f : C((↑X : Type u_1), R)) ↦ (⇑f : (a : (↑X : Type u_1)) → R)) ''
          (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)))
        f ∧
      f x ≠ f y

Tactic:
⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, ?_⟩⟩

Premises used: Algebra.mem_top, And.intro, Exists.intro, Polynomial.X, rfl
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x y : (↑X : Type u_1)
h : x ≠ y
refine :
  Ne.{u_1 + 1} (α := R)
    ((fun (f : C((↑X : Type u_1), R)) ↦ ((⇑f : (a : (↑X : Type u_1)) → R) : (a : (↑X : Type u_1)) → R))
      (((↑(toContinuousMapOnAlgHom X) : R[X] →+* C((↑X : Type u_1), R)) : (a : R[X]) → C((↑X : Type u_1), R))
        Polynomial.X)
      x)
    ((fun (f : C((↑X : Type u_1), R)) ↦ ((⇑f : (a : (↑X : Type u_1)) → R) : (a : (↑X : Type u_1)) → R))
      (((↑(toContinuousMapOnAlgHom X) : R[X] →+* C((↑X : Type u_1), R)) : (a : R[X]) → C((↑X : Type u_1), R))
        Polynomial.X)
      y)
⊢ ∃ (f : (↑X : Type u_1) → R),
    Membership.mem (γ := Set ((↑X : Type u_1) → R))
        ((fun (f : C((↑X : Type u_1), R)) ↦ (⇑f : (a : (↑X : Type u_1)) → R)) ''
          (↑(polynomialFunctions X) : Set C((↑X : Type u_1), R)))
        f ∧
      f x ≠ f y

Tactic:
refine ⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, ?_⟩⟩
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x y : (↑X : Type u_1)
h : x ≠ y
simp : ¬(↑x : R) = (↑y : R)
⊢ ¬eval (↑x : R) Polynomial.X = eval (↑y : R) Polynomial.X

Tactic:
simp only [Polynomial.eval_X]

Premises used: Polynomial.eval_X
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x y : (↑X : Type u_1)
h : x ≠ y
⊢ ¬(↑x : R) = (↑y : R)

Tactic:
fun h' => h (Subtype.ext h')

Premises used: Not, Subtype.ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
X : Set R
x y : (↑X : Type u_1)
h : x ≠ y
⊢ ¬(↑x : R) = (↑y : R)

Tactic:
exact fun h' => h (Subtype.ext h')

Premises used: Subtype.ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
h₁ :
  ∀ (f : C((↑(Set.Icc a b) : Type), ℝ)),
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
        (Subalgebra.comap
          (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
          (polynomialFunctions I))
        f ↔
      Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.comap
      (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
      (polynomialFunctions I))
    (polynomialFunctions (Set.Icc a b))

Tactic:
ext f
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
h₁ :
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.comap
        (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
        (polynomialFunctions I))
      f →
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f
h₂ :
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f →
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.comap
        (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
        (polynomialFunctions I))
      f
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.comap
        (compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type))))
        (polynomialFunctions I))
      f ↔
    Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f

Tactic:
fconstructor
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  Eq (α := C((↑I : Type), ℝ))
    (((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) p :
      C((↑I : Type), ℝ))
    (((↑(compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))) :
            C((↑(Set.Icc a b) : Type), ℝ) →+* C((↑I : Type), ℝ)) :
          (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
        f :
      C((↑I : Type), ℝ))
⊢ ∀ (x : (↑I : Type)),
    Eq (α := ℝ)
      (((((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) p :
              C((↑I : Type), ℝ)) :
            (a : (↑I : Type)) → ℝ)
          x :
        ℝ)
      (((((↑(compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))) :
                    C((↑(Set.Icc a b) : Type), ℝ) →+* C((↑I : Type), ℝ)) :
                  (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
                f :
              C((↑I : Type), ℝ)) :
            (a : (↑I : Type)) → ℝ)
          x :
        ℝ)

Tactic:
rw [DFunLike.ext_iff] at w

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f

Tactic:
⟨q, ⟨?_, ?_⟩⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
h₁ : q ∈ (↑(Subalgebra.toSubsemiring (R := ℝ) ⊤) : Set ℝ[X])
h₂ :
  ((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
        (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
      q =
    f
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) (polynomialFunctions (Set.Icc a b)) f

Tactic:
refine ⟨q, ⟨?_, ?_⟩⟩
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
⊢ q ∈ (↑(Subalgebra.toSubsemiring (R := ℝ) ⊤) : Set ℝ[X])

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
h₁ :
  ∀ (x : (↑(Set.Icc a b) : Type)),
    Eq (α := ℝ)
      (((((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
                  (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
                q :
              C((↑(Set.Icc a b) : Type), ℝ)) :
            (a : (↑(Set.Icc a b) : Type)) → ℝ)
          x :
        ℝ)
      ((f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x : ℝ)
⊢ ((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
        (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
      q =
    f

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
h₁ : Polynomial.eval ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) p = (f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x
⊢ Eq (α := ℝ)
    (((((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
                (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
              q :
            C((↑(Set.Icc a b) : Type), ℝ)) :
          (a : (↑(Set.Icc a b) : Type)) → ℝ)
        x :
      ℝ)
    ((f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x : ℝ)

Tactic:
simp only [q, neg_mul, map_neg, 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.eval_comp, Polynomial.toContinuousMapOnAlgHom_apply,
        Polynomial.toContinuousMapOn_apply, Polynomial.toContinuousMap_apply]

Premises used: AlgHom.coe_toRingHom, Polynomial.toContinuousMap_apply, Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_mul, map_neg, map_mul, Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_smul, neg_mul, Polynomial.eval_neg, smul_eq_mul, Polynomial.toContinuousMapOn_apply, Polynomial.toContinuousMapOnAlgHom_apply
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
⊢ Polynomial.eval (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) ⋯) : ℝ) p =
    (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
      ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type))
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) ⋯) :
        (↑(Set.Icc a b) : Type))

Tactic:
w ⟨_, _⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
h₁ :
  x =
    (Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type))
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) ⋯)
h₂ : (b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹) ∈ I
⊢ Polynomial.eval ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) p = (f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x

Tactic:
convert! w ⟨_, _⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
h₁ :
  (↑x : ℝ) =
    (↑((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type))
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) ⋯)) :
      ℝ)
⊢ x =
    (Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type))
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) ⋯)

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
⊢ b - a ≠ 0

Tactic:
replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h_1 : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h_1) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
h : b - a ≠ 0
⊢ (↑x : ℝ) = (b - a) * ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) + a

Tactic:
field
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
h₁ : ((↑x : ℝ) - a) * (b - a)⁻¹ ∈ I
⊢ (b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹) ∈ I

Tactic:
rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]

Premises used: add_mul, sub_eq_add_neg, HSub.hSub, Inv.inv, mul_comm, neg_mul
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
⊢ 0 < (b - a)⁻¹

Tactic:
have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
w₁ : 0 < (b - a)⁻¹
⊢ 0 ≤ (↑x : ℝ) - a

Tactic:
have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
f : C((↑(Set.Icc a b) : Type), ℝ)
p : ℝ[X]
w :
  ∀ (x : (↑I : Type)),
    Polynomial.eval (↑x : ℝ) p =
      (f : (a : (↑(Set.Icc a b) : Type)) → ℝ)
        ((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑I : Type)) → (↑(Set.Icc a b) : Type)) x :
          (↑(Set.Icc a b) : Type))
q : ℝ[X] :=
  p.comp
    (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a)⁻¹ X)
      ((Polynomial.C : (a : ℝ) → ℝ[X]) (-a * (b - a)⁻¹) : ℝ[X]))
x : (↑(Set.Icc a b) : Type)
w₁ : 0 < (b - a)⁻¹
w₂ : 0 ≤ (↑x : ℝ) - a
⊢ (↑x : ℝ) - a ≤ b - a

Tactic:
have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a