awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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)⁻¹)) ⋯)
⊢ Polynomial.eval ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) p = (f : (a : (↑(Set.Icc a b) : Type)) → ℝ) x
have h₂ : (b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹) ∈ I
Tactic: convert! w ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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)
⊢ 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)⁻¹)) ⋯)
have 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)⁻¹)) sorry)) :
    ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (hypothesis)
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)
⊢ (↑x : ℝ) = (b - a) * ((b - a)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹)) + a
have h₁ : b - a ≠ 0
Tactic: replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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)⁻¹ * (↑x : ℝ) + -(a * (b - a)⁻¹) ∈ I
have h₁ : ((↑x : ℝ) - a) * (b - a)⁻¹ ∈ I
Tactic: rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (hypothesis)
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)
⊢ ((↑x : ℝ) - a) * (b - a)⁻¹ ∈ I
have w₁ : 0 < (b - a)⁻¹
Tactic: have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (hypothesis)
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)⁻¹
⊢ ((↑x : ℝ) - a) * (b - a)⁻¹ ∈ I
have w₂ : 0 ≤ (↑x : ℝ) - a
Tactic: have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (hypothesis)
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)⁻¹ ∈ I
have w₃ : (↑x : ℝ) - a ≤ b - a
Tactic: have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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)⁻¹ ∈ I
have h₁ : 0 ≤ ((↑x : ℝ) - a) * (b - a)⁻¹
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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)⁻¹
⊢ ((↑x : ℝ) - a) * (b - a)⁻¹ ∈ I
have h₂ : ((↑x : ℝ) - a) * (b - a)⁻¹ ≤ 1
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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), ℝ))
have h₁ : q ∈ (↑(Subalgebra.toSubsemiring (R := ℝ) ⊤) : Set ℝ[X])
Tactic: refine ⟨q, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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])
⊢ 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), ℝ))
have 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), ℝ))
Tactic: refine ⟨q, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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]))
⊢ 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), ℝ))
have 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 :
      ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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))]
have 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))]
Tactic: refine le_antisymm ?_
    (Algebra.adjoin_le fun _ h => ⟨X, trivial, (Set.mem_singleton_iff.1 h).symm⟩)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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))
have 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))
Tactic: refine p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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))
⊢ 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))
have 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))
Tactic: refine p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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))
⊢ 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))
have 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))
Tactic: refine p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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))]
    ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) ((Polynomial.C : (a : R) → R[X]) r) :
      C((↑s : Type u_1), R))
have 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))
Tactic: rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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 (α := 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))
have 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)))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
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 (α := 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))
have 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)))
Tactic: rw [pow_succ, ← mul_assoc, map_mul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
A : Type u_2
inst_3 : Semiring A
inst_4 : Algebra R A
s : Set R
φ ψ : C((↑s : Type u_1), R) →ₐ[R] A
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑s : Type u_1), R)) → A)
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R)) :
      A)
    ((ψ : (a : C((↑s : Type u_1), R)) → A)
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R)) :
      A)
⊢ LE.le (α := Subalgebra R C((↑s : Type u_1), R)) (polynomialFunctions s) (AlgHom.equalizer φ ψ)
have rw : LE.le (α := 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))] (AlgHom.equalizer φ ψ)
Tactic: rw [polynomialFunctions.eq_adjoin_X s]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : StarRing R
inst_4 : ContinuousStar R
s : Set R
⊢ Eq (α := StarSubalgebra R C((↑s : Type u_1), R)) (Subalgebra.starClosure (polynomialFunctions s))
    (adjoin R
      (singleton (α := C((↑s : Type u_1), R))
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))))
have rw : Eq (α := StarSubalgebra R C((↑s : Type u_1), R))
  (Subalgebra.starClosure
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))])
  (adjoin R
    (singleton (α := 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: rw [polynomialFunctions.eq_adjoin_X s, adjoin_eq_starClosure_adjoin]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : StarRing R
inst_4 : ContinuousStar R
s : Set R
rw :
  Eq (α := StarSubalgebra R C((↑s : Type u_1), R))
    (Subalgebra.starClosure
      R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))])
    (adjoin R
      (singleton (α := C((↑s : Type u_1), R))
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))))
⊢ Eq (α := StarSubalgebra R C((↑s : Type u_1), R)) (Subalgebra.starClosure (polynomialFunctions s))
    (adjoin R
      (singleton (α := C((↑s : Type u_1), R))
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))))
have rw₁ : Eq (α := StarSubalgebra R C((↑s : Type u_1), R))
  (Subalgebra.starClosure
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))])
  (Subalgebra.starClosure
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))])
Tactic: rw [polynomialFunctions.eq_adjoin_X s, adjoin_eq_starClosure_adjoin]