awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
w₃ : (↑x : ℝ) - a ≤ b - a
h₁ : 0 ≤ ((↑x : ℝ) - a) * (b - a)⁻¹
h₂ : ((↑x : ℝ) - a) * (b - a)⁻¹ ≤ 1
⊢ ((↑x : ℝ) - a) * (b - a)⁻¹ ∈ I

Tactic:
fconstructor
-- 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
w₃ : (↑x : ℝ) - a ≤ b - a
⊢ 0 ≤ ((↑x : ℝ) - a) * (b - a)⁻¹

Tactic:
mul_nonneg w₂ (le_of_lt w₁)

Premises used: mul_nonneg, le_of_lt
-- 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
w₃ : (↑x : ℝ) - a ≤ b - a
⊢ 0 ≤ ((↑x : ℝ) - a) * (b - a)⁻¹

Tactic:
exact mul_nonneg w₂ (le_of_lt w₁)

Premises used: mul_nonneg, le_of_lt
-- 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
w₃ : (↑x : ℝ) - a ≤ b - a
h₁ : (↑x : ℝ) - a ≤ b - a
⊢ ((↑x : ℝ) - a) * (b - a)⁻¹ ≤ 1

Tactic:
rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]

Premises used: Iff.mpr, sub_pos, div_eq_mul_inv, div_le_one
-- 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
w₃ : (↑x : ℝ) - a ≤ b - a
⊢ (↑x : ℝ) - a ≤ b - a

Tactic:
w₃
-- 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
w₃ : (↑x : ℝ) - a ≤ b - a
⊢ (↑x : ℝ) - a ≤ b - a

Tactic:
exact w₃
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] :=
  p.comp (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a) X) ((Polynomial.C : (a : ℝ) → ℝ[X]) a : ℝ[X]))
⊢ Membership.mem (α := C((↑(Set.Icc a b) : Type), ℝ)) (γ := 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))
    (((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
          (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
        p :
      C((↑(Set.Icc a b) : Type), ℝ))

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

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] :=
  p.comp (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a) X) ((Polynomial.C : (a : ℝ) → ℝ[X]) a : ℝ[X]))
h₁ : q ∈ (↑(Subalgebra.toSubsemiring (R := ℝ) ⊤) : Set ℝ[X])
h₂ :
  Eq (α := C((↑I : Type), ℝ))
    (((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) q :
      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), ℝ))
        (((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
            (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
          p) :
      C((↑I : Type), ℝ))
⊢ Membership.mem (α := C((↑(Set.Icc a b) : Type), ℝ)) (γ := 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))
    (((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
          (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
        p :
      C((↑(Set.Icc a b) : Type), ℝ))

Tactic:
refine ⟨q, ⟨?_, ?_⟩⟩
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] :=
  p.comp (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a) X) ((Polynomial.C : (a : ℝ) → ℝ[X]) a : ℝ[X]))
⊢ q ∈ (↑(Subalgebra.toSubsemiring (R := ℝ) ⊤) : Set ℝ[X])

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] :=
  p.comp (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a) X) ((Polynomial.C : (a : ℝ) → ℝ[X]) a : ℝ[X]))
h₁ :
  ∀ (x : (↑I : Type)),
    Eq (α := ℝ)
      (((((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) q :
              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), ℝ))
                (((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
                    (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
                  p) :
              C((↑I : Type), ℝ)) :
            (a : (↑I : Type)) → ℝ)
          x :
        ℝ)
⊢ Eq (α := C((↑I : Type), ℝ))
    (((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) q :
      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), ℝ))
        (((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
            (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
          p) :
      C((↑I : Type), ℝ))

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] :=
  p.comp (HAdd.hAdd (β := ℝ[X]) (HSMul.hSMul (β := ℝ[X]) (b - a) X) ((Polynomial.C : (a : ℝ) → ℝ[X]) a : ℝ[X]))
x : (↑I : Type)
⊢ Eq (α := ℝ)
    (((((↑(toContinuousMapOnAlgHom I) : ℝ[X] →+* C((↑I : Type), ℝ)) : (a : ℝ[X]) → C((↑I : Type), ℝ)) q :
            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), ℝ))
              (((↑(toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
                  (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
                p) :
            C((↑I : Type), ℝ)) :
          (a : (↑I : Type)) → ℝ)
        x :
      ℝ)

Tactic:
simp [q, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
⊢ Eq (α := Subalgebra R C((↑s : Type u_1), R)) (polynomialFunctions s)
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]

Tactic:
le_antisymm ?_
    (Algebra.adjoin_le fun _ h => ⟨X, trivial, (Set.mem_singleton_iff.1 h).symm⟩)

Premises used: trivial, le_antisymm, Set.mem_singleton_iff, And.intro, Algebra.adjoin_le, Exists.intro, Iff.mp, Eq.symm, Polynomial.X
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
refine :
  LE.le (α := Subalgebra R C((↑s : Type u_1), R)) (polynomialFunctions s)
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
⊢ Eq (α := Subalgebra R C((↑s : Type u_1), R)) (polynomialFunctions s)
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]

Tactic:
refine le_antisymm ?_
    (Algebra.adjoin_le fun _ h => ⟨X, trivial, (Set.mem_singleton_iff.1 h).symm⟩)
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
⊢ Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) p : C((↑s : Type u_1), R))

Tactic:
p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_

Premises used: Polynomial.induction_on
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
refine_1 :
  ∀ (r : R),
    Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
      R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) ((Polynomial.C : (a : R) → R[X]) r) :
        C((↑s : Type u_1), R))
refine_2 :
  ∀ (f g : R[X])
    (hf :
      Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
        R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) f : C((↑s : Type u_1), R)))
    (hg :
      Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
        R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) g : C((↑s : Type u_1), R))),
    Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
      R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) (f + g) : C((↑s : Type u_1), R))
refine_3 :
  ∀ (n : ℕ) (r : R)
    (hn :
      Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
        R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
            (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
          C((↑s : Type u_1), R))),
    Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
      R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
        C((↑s : Type u_1), R))
⊢ Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) p : C((↑s : Type u_1), R))

Tactic:
refine p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
refine_1 :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((algebraMap R C((↑s : Type u_1), R) : (a : R) → C((↑s : Type u_1), R)) r : C((↑s : Type u_1), R))
⊢ Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) ((Polynomial.C : (a : R) → R[X]) r) :
      C((↑s : Type u_1), R))

Tactic:
rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]

Premises used: Polynomial.C_eq_algebraMap, AlgHomClass.commutes
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((algebraMap R C((↑s : Type u_1), R) : (a : R) → C((↑s : Type u_1), R)) r : C((↑s : Type u_1), R))

Tactic:
Subalgebra.algebraMap_mem _ r

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
r : R
⊢ Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((algebraMap R C((↑s : Type u_1), R) : (a : R) → C((↑s : Type u_1), R)) r : C((↑s : Type u_1), R))

Tactic:
exact Subalgebra.algebraMap_mem _ r

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) f : C((↑s : Type u_1), R))
hg :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) g : C((↑s : Type u_1), R))
refine_2 :
  Membership.mem (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (HAdd.hAdd (α := C((↑s : Type u_1), R)) (β := C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) f : C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) g : C((↑s : Type u_1), R)))
⊢ Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) (f + g) : C((↑s : Type u_1), R))

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) f : C((↑s : Type u_1), R))
hg :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) g : C((↑s : Type u_1), R))
⊢ Membership.mem (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (HAdd.hAdd (α := C((↑s : Type u_1), R)) (β := C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) f : C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) g : C((↑s : Type u_1), R)))

Tactic:
add_mem hf hg

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p f g : R[X]
hf :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) f : C((↑s : Type u_1), R))
hg :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) g : C((↑s : Type u_1), R))
⊢ Membership.mem (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (HAdd.hAdd (α := C((↑s : Type u_1), R)) (β := C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) f : C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) g : C((↑s : Type u_1), R)))

Tactic:
exact add_mem hf hg

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      C((↑s : Type u_1), R))
refine_3 :
  Membership.mem (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (HMul.hMul (α := C((↑s : Type u_1), R)) (β := C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
        C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R)))
⊢ Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      C((↑s : Type u_1), R))

Tactic:
rw [pow_succ, ← mul_assoc, map_mul]

Premises used: pow_succ, mul_assoc, map_mul
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      C((↑s : Type u_1), R))
⊢ Membership.mem (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (HMul.hMul (α := C((↑s : Type u_1), R)) (β := C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
        C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R)))

Tactic:
mul_mem hn (Algebra.subset_adjoin <| Set.mem_singleton _)

Premises used: Set.mem_singleton, Algebra.subset_adjoin, MulMemClass.mul_mem
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
p : R[X]
n : ℕ
r : R
hn :
  Membership.mem (α := C((↑s : Type u_1), R)) (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      C((↑s : Type u_1), R))
⊢ Membership.mem (γ := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (HMul.hMul (α := C((↑s : Type u_1), R)) (β := C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R))
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
        C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R)))

Tactic:
exact mul_mem hn (Algebra.subset_adjoin <| Set.mem_singleton _)

Premises used: Set.mem_singleton, Algebra.subset_adjoin, MulMemClass.mul_mem