awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (goal)
Goal:
X : Type u_1
𝕜 : Type u_4
inst : TopologicalSpace X
inst_1 : NormedField 𝕜
inst_2 : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ spectrum 𝕜 f = Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜)
have rw : Eq (α := Set 𝕜)
  (Set.preimage (β := 𝕜) (⇑(RingHom.id 𝕜) : (a : 𝕜) → 𝕜) (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜)))
  (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜))
Tactic: rw [spectrum_eq_preimage_range, Algebra.algebraMap_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
⊢ Eq (α := Subalgebra ℝ C((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) ⊤
have h : LE.le (α := Subalgebra ℝ C((↑I : Type), ℝ)) ⊤ (Subalgebra.topologicalClosure (polynomialFunctions I))
Tactic: apply top_unique
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
f : C((↑I : Type), ℝ)
⊢ Membership.mem (γ := Subalgebra ℝ C((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) f
have h : ∀ (n : ℕ), bernsteinApproximation n f ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions I)) : Set C((↑I : Type), ℝ))
Tactic: refine mem_closure_of_tendsto (bernsteinApproximation_uniform f) <| .of_forall fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions I)) : Set C((↑I : Type), ℝ))
have h : ∀ (x : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ x →
    Membership.mem (γ := Subalgebra ℝ C((↑I : Type), ℝ)) (polynomialFunctions I)
      (HSMul.hSMul (β := C((↑I : Type), ℝ)) (bernstein n (↑x : ℕ))
        (const (↑I : Type) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z x)) : C((↑I : Type), ℝ)))
Tactic: apply Subalgebra.sum_mem
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
i : Fin (n + 1)
⊢ Membership.mem (γ := Subalgebra ℝ C((↑I : Type), ℝ)) (polynomialFunctions I)
    (HSMul.hSMul (β := C((↑I : Type), ℝ)) (bernstein n (↑i : ℕ))
      (const (↑I : Type) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : C((↑I : Type), ℝ)))
have h : Membership.mem (γ := Set C((↑I : Type), ℝ))
  (Set.range (ι := Polynomial ℝ) (⇑(Polynomial.toContinuousMapOnAlgHom I) : (a : Polynomial ℝ) → C((↑I : Type), ℝ)))
  (HSMul.hSMul (β := C((↑I : Type), ℝ)) (bernstein n (↑i : ℕ))
    (const (↑I : Type) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : C((↑I : Type), ℝ)))
Tactic: rw [← SetLike.mem_coe, polynomialFunctions_coe]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
i : Fin (n + 1)
⊢ Membership.mem (γ := Set C((↑I : Type), ℝ))
    (Set.range (ι := Polynomial ℝ) (⇑(Polynomial.toContinuousMapOnAlgHom I) : (a : Polynomial ℝ) → C((↑I : Type), ℝ)))
    (HSMul.hSMul (β := C((↑I : Type), ℝ)) (bernstein n (↑i : ℕ))
      (const (↑I : Type) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : C((↑I : Type), ℝ)))
have h : (Polynomial.toContinuousMapOnAlgHom I : (a : Polynomial ℝ) → C((↑I : Type), ℝ))
    (HMul.hMul (α := Polynomial ℝ) (β := Polynomial ℝ) (bernsteinPolynomial ℝ n (↑i : ℕ))
      ((Polynomial.C : (a : ℝ) → Polynomial ℝ) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : Polynomial ℝ)) =
  HSMul.hSMul (β := C((↑I : Type), ℝ)) (bernstein n (↑i : ℕ))
    (const (↑I : Type) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : C((↑I : Type), ℝ))
Tactic: use bernsteinPolynomial ℝ n i * .C (f (bernstein.z i))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
i : Fin (n + 1)
⊢ (Polynomial.toContinuousMapOnAlgHom I : (a : Polynomial ℝ) → C((↑I : Type), ℝ))
      (HMul.hMul (α := Polynomial ℝ) (β := Polynomial ℝ) (bernsteinPolynomial ℝ n (↑i : ℕ))
        ((Polynomial.C : (a : ℝ) → Polynomial ℝ) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : Polynomial ℝ)) =
    HSMul.hSMul (β := C((↑I : Type), ℝ)) (bernstein n (↑i : ℕ))
      (const (↑I : Type) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : C((↑I : Type), ℝ))
have h : ∀ (a : (↑I : Type)),
  Eq (α := ℝ)
    ((((Polynomial.toContinuousMapOnAlgHom I : (a : Polynomial ℝ) → C((↑I : Type), ℝ))
              (HMul.hMul (α := Polynomial ℝ) (β := Polynomial ℝ) (bernsteinPolynomial ℝ n (↑i : ℕ))
                ((Polynomial.C : (a : ℝ) → Polynomial ℝ) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) :
                  Polynomial ℝ)) :
            C((↑I : Type), ℝ)) :
          (a : (↑I : Type)) → ℝ)
        a :
      ℝ)
    ((HSMul.hSMul (β := C((↑I : Type), ℝ)) (bernstein n (↑i : ℕ))
            (const (↑I : Type) ((f : (a : (↑I : Type)) → ℝ) (bernstein.z i)) : C((↑I : Type), ℝ)) :
          (a : (↑I : Type)) → ℝ)
        a :
      ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
a b : ℝ
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
have inl : ∀ (h : a < b),
  Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
Tactic: rcases lt_or_ge a b with h | h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
a b : ℝ
inl :
  ∀ (h : a < b),
    Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
have inr : ∀ (h : b ≤ a),
  Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
Tactic: rcases lt_or_ge a b with h | h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
h : a < b
W : C((↑(Set.Icc a b) : Type), ℝ) →ₐ[ℝ] C((↑I : Type), ℝ) :=
  compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))
W' : C((↑(Set.Icc a b) : Type), ℝ) ≃ₜ C((↑I : Type), ℝ) := Homeomorph.arrowCongr (iccHomeoI a b h) (Homeomorph.refl ℝ)
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
have w : Eq (α := (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
  (⇑W : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
  (⇑W' : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
Tactic: have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
h : a < b
W : C((↑(Set.Icc a b) : Type), ℝ) →ₐ[ℝ] C((↑I : Type), ℝ) :=
  compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))
W' : C((↑(Set.Icc a b) : Type), ℝ) ≃ₜ C((↑I : Type), ℝ) := Homeomorph.arrowCongr (iccHomeoI a b h) (Homeomorph.refl ℝ)
w :
  Eq (α := (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W' : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
have p : Eq (α := Subalgebra ℝ C((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) ⊤
Tactic: have p := polynomialFunctions_closure_eq_top'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
h : a < b
W : C((↑(Set.Icc a b) : Type), ℝ) →ₐ[ℝ] C((↑I : Type), ℝ) :=
  compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))
W' : C((↑(Set.Icc a b) : Type), ℝ) ≃ₜ C((↑I : Type), ℝ) := Homeomorph.arrowCongr (iccHomeoI a b h) (Homeomorph.refl ℝ)
w :
  Eq (α := (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W' : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
p : Eq (α := Subalgebra ℝ C((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) ⊤
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
have p₁ : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = Subalgebra.comap W ⊤
Tactic: apply_fun fun s => s.comap W at p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
h : a < b
W : C((↑(Set.Icc a b) : Type), ℝ) →ₐ[ℝ] C((↑I : Type), ℝ) :=
  compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))
W' : C((↑(Set.Icc a b) : Type), ℝ) ≃ₜ C((↑I : Type), ℝ) := Homeomorph.arrowCongr (iccHomeoI a b h) (Homeomorph.refl ℝ)
w :
  Eq (α := (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W' : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
p : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = Subalgebra.comap W ⊤
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
have p₁ : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = ⊤
Tactic: simp only [Algebra.comap_top] at p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
h : a < b
W : C((↑(Set.Icc a b) : Type), ℝ) →ₐ[ℝ] C((↑I : Type), ℝ) :=
  compRightAlgHom ℝ ℝ (↑(Homeomorph.symm (iccHomeoI a b h)) : C((↑I : Type), (↑(Set.Icc a b) : Type)))
W' : C((↑(Set.Icc a b) : Type), ℝ) ≃ₜ C((↑I : Type), ℝ) := Homeomorph.arrowCongr (iccHomeoI a b h) (Homeomorph.refl ℝ)
w :
  Eq (α := (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
    (⇑W' : (a : C((↑(Set.Icc a b) : Type), ℝ)) → C((↑I : Type), ℝ))
p : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = ⊤
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
have p₁ : (Subalgebra.comap W (polynomialFunctions I)).topologicalClosure = ⊤
Tactic: rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) f
have rw : Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) ⊤ f
Tactic: rw [polynomialFunctions_closure_eq_top _ _]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
have w : ∃ᶠ (x : C((↑(Set.Icc a b) : Type), ℝ)) in nhds f,
  x ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc a b))) : Set C((↑(Set.Icc a b) : Type), ℝ))
Tactic: have w := mem_closure_iff_frequently.mp (continuousMap_mem_polynomialFunctions_closure _ _ f)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
ε : ℝ
pos : 0 < ε
w :
  ∃ᶠ (x : C((↑(Set.Icc a b) : Type), ℝ)) in nhds f,
    x ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc a b))) : Set C((↑(Set.Icc a b) : Type), ℝ))
⊢ ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
have w₁ : ∀ (i : ℝ),
  0 < i →
    ∃ x ∈ Metric.ball f i,
      x ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc a b))) : Set C((↑(Set.Icc a b) : Type), ℝ))
Tactic: rw [Metric.nhds_basis_ball.frequently_iff] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
ε : ℝ
pos : 0 < ε
w :
  ∀ (i : ℝ),
    0 < i →
      ∃ x ∈ Metric.ball f i,
        x ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc a b))) : Set C((↑(Set.Icc a b) : Type), ℝ))
⊢ ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
have obtain : ∀ (m : ℝ[X])
  (H :
    Membership.mem (α := C((↑(Set.Icc a b) : Type), ℝ)) (Metric.ball f ε)
      (((↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
            (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
          m :
        C((↑(Set.Icc a b) : Type), ℝ))),
  ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
Tactic: obtain ⟨-, H, ⟨m, ⟨-, rfl⟩⟩⟩ := w ε pos
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
ε : ℝ
pos : 0 < ε
w :
  ∀ (i : ℝ),
    0 < i →
      ∃ x ∈ Metric.ball f i,
        x ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc a b))) : Set C((↑(Set.Icc a b) : Type), ℝ))
m : ℝ[X]
H :
  Membership.mem (α := C((↑(Set.Icc a b) : Type), ℝ)) (Metric.ball f ε)
    (((↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
          (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
        m :
      C((↑(Set.Icc a b) : Type), ℝ))
⊢ ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
have H₁ : ‖HSub.hSub (α := C((↑(Set.Icc a b) : Type), ℝ))
      (((↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) : ℝ[X] →+* C((↑(Set.Icc a b) : Type), ℝ)) :
            (a_1 : ℝ[X]) → C((↑(Set.Icc a b) : Type), ℝ))
          m :
        C((↑(Set.Icc a b) : Type), ℝ))
      f‖ <
  ε
Tactic: rw [Metric.mem_ball, dist_eq_norm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
f' : C((↑(Set.Icc a b) : Type), ℝ) := { toFun := fun (x : (↑(Set.Icc a b) : Type)) ↦ f (↑x : ℝ), continuous_toFun := ⋯ }
⊢ ∃ (p : ℝ[X]), ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε
have obtain : ∀ (p : ℝ[X]) (b_1 : ‖p.toContinuousMapOn (Set.Icc a b) - f'‖ < ε),
  ∃ (p : ℝ[X]), ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε
Tactic: obtain ⟨p, b⟩ := exists_polynomial_near_continuousMap a b f' ε pos
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (goal)
Goal:
a b_1 : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b_1)
ε : ℝ
pos : 0 < ε
f' : C((↑(Set.Icc a b_1) : Type), ℝ) :=
  { toFun := fun (x : (↑(Set.Icc a b_1) : Type)) ↦ f (↑x : ℝ), continuous_toFun := ⋯ }
p : ℝ[X]
b : ‖p.toContinuousMapOn (Set.Icc a b_1) - f'‖ < ε
⊢ ∃ (p : ℝ[X]), ∀ x ∈ Set.Icc a b_1, |Polynomial.eval x p - f x| < ε
have h : ∀ x ∈ Set.Icc a b_1, |Polynomial.eval x p - f x| < ε
Tactic: use p
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Weierstrass (hypothesis)
Goal:
a b_1 : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b_1)
ε : ℝ
pos : 0 < ε
f' : C((↑(Set.Icc a b_1) : Type), ℝ) :=
  { toFun := fun (x : (↑(Set.Icc a b_1) : Type)) ↦ f (↑x : ℝ), continuous_toFun := ⋯ }
p : ℝ[X]
b : ‖p.toContinuousMapOn (Set.Icc a b_1) - f'‖ < ε
⊢ ∀ x ∈ Set.Icc a b_1, |Polynomial.eval x p - f x| < ε
have b₁ : ∀ (x : (↑(Set.Icc a b_1) : Type)),
  norm (E := ℝ) ((p.toContinuousMapOn (Set.Icc a b_1) - f' : (a : (↑(Set.Icc a b_1) : Type)) → ℝ) x : ℝ) < ε
Tactic: rw [norm_lt_iff _ pos] at b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : Eq (α := (a : α) → β) ((fun (f : α →C₀ β) ↦ f.toFun) f) ((fun (f : α →C₀ β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (continuous_toFun : Continuous[inst, inst_1] toFun)
  (zero_at_infty' :
    Tendsto { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun (cocompact α) (𝓝 0))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →C₀ β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, zero_at_infty' := zero_at_infty' })
      ((fun (f : α →C₀ β) ↦ f.toFun) g)),
  { toFun := toFun, continuous_toFun := continuous_toFun, zero_at_infty' := zero_at_infty' : α →C₀ β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
g : α →C₀ β
toFun : α → β
continuous_toFun : Continuous[inst, inst_1] toFun
zero_at_infty' : Tendsto { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun (cocompact α) (𝓝 0)
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →C₀ β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, zero_at_infty' := zero_at_infty' })
    ((fun (f : α →C₀ β) ↦ f.toFun) g)
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, zero_at_infty' := zero_at_infty' : α →C₀ β } = g
have obtain : ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous[inst, inst_1] toFun_1)
  (zero_at_infty'_1 :
    Tendsto { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun (cocompact α) (𝓝 0))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →C₀ β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, zero_at_infty' := zero_at_infty' })
      ((fun (f : α →C₀ β) ↦ f.toFun)
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1, zero_at_infty' := zero_at_infty'_1 })),
  { toFun := toFun, continuous_toFun := continuous_toFun, zero_at_infty' := zero_at_infty' : α →C₀ β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, zero_at_infty' := zero_at_infty'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous[inst, inst_1] f'
have rw : Continuous[inst, inst_1] (⇑f : (a : α) → β)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Tendsto f' (cocompact α) (𝓝 0)
have simp_rw : Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)
Tactic: simp_rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
⊢ (r • f) • g = r • f • g
have h : ∀ (x : α), Eq.{v + 1} (α := β) (((r • f) • g : (a : α) → β) x : β) ((r • f • g : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
x_1 : α
⊢ Eq.{v + 1} (α := β) (((r • f) • g : (a : α) → β) x_1 : β) ((r • f • g : (a : α) → β) x_1 : β)
have h : HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
  r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: simp only [smul_eq_mul, coe_mul, coe_smul, Pi.mul_apply, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
x_1 : α
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
have h : HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
  r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
have h₁ : HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
h₁ :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
have h₂ : r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
⊢ r • f • g = f • r • g
have h : ∀ (x : α), Eq.{v + 1} (α := β) ((r • f • g : (a : α) → β) x : β) ((f • r • g : (a : α) → β) x : β)
Tactic: ext