awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
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), ℝ)))
⊢ bernsteinApproximation n f ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions I)) : Set C((↑I : Type), ℝ))

Tactic:
apply Subalgebra.sum_mem

Premises used: Subalgebra.sum_mem
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
i : Fin (n + 1)
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), ℝ)))
⊢ 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), ℝ)))

Tactic:
rw [← SetLike.mem_coe, polynomialFunctions_coe]

Premises used: polynomialFunctions_coe, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
i : Fin (n + 1)
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), ℝ))
⊢ 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:
use bernsteinPolynomial ℝ n i * .C (f (bernstein.z i))

Premises used: Real, Fin.val, bernsteinPolynomial
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
i : Fin (n + 1)
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 :
        ℝ)
⊢ (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:
ext
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
f : C((↑I : Type), ℝ)
n : ℕ
i : Fin (n + 1)
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:
simp [bernstein]

Premises used: bernstein
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
a b : ℝ
inl :
  ∀ (h : a < b),
    Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
      (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤
inr :
  ∀ (h : b ≤ a),
    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))) ⊤

Tactic:
rcases lt_or_ge a b with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 (α := (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
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) ⊤

Tactic:
have p := polynomialFunctions_closure_eq_top'
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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)) ⊤
⊢ Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = Subalgebra.comap W ⊤

Tactic:
apply_fun fun s => s.comap W at p
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 ⊤
⊢ Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = ⊤

Tactic:
simp only [Algebra.comap_top] at p

Premises used: Algebra.comap_top
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 (polynomialFunctions I)).topologicalClosure = ⊤

Tactic:
rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p

Premises used: Subalgebra.topologicalClosure_comap_homeomorph
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 (polynomialFunctions I)).topologicalClosure = ⊤
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤

Tactic:
rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p

Premises used: polynomialFunctions.comap_compRightAlgHom_iccHomeoI
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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((↑(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))) ⊤

Tactic:
p
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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((↑(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))) ⊤

Tactic:
exact p
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
a b : ℝ
h : b ≤ a
⊢ Eq (α := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) ⊤

Tactic:
subsingleton [(Set.subsingleton_Icc_of_ge h).coe_sort]

Premises used: Set.Subsingleton.coe_sort, Set.subsingleton_Icc_of_ge
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
rw : Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) ⊤ f
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))) f

Tactic:
rw [polynomialFunctions_closure_eq_top _ _]

Premises used: polynomialFunctions_closure_eq_top
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
⊢ Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc a b) : Type), ℝ)) ⊤ f

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
a b : ℝ
f : C((↑(Set.Icc a b) : Type), ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ᶠ (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)
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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), ℝ))
⊢ ∀ (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

Premises used: Filter.HasBasis.frequently_iff, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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), ℝ))
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‖ < ε
⊢ ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
obtain ⟨-, H, ⟨m, ⟨-, rfl⟩⟩⟩ := w ε pos

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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), ℝ))
⊢ ‖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

Premises used: dist_eq_norm, Metric.mem_ball
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 :
  ‖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‖ <
    ε
⊢ ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
⟨m, H⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 :
  ‖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‖ <
    ε
⊢ ∃ (p : ℝ[X]), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
exact ⟨m, H⟩
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 := ⋯ }
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| < ε
⊢ ∃ (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

Premises used: exists_polynomial_near_continuousMap
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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'‖ < ε
h : ∀ x ∈ Set.Icc a b_1, |Polynomial.eval x p - f x| < ε
⊢ ∃ (p : ℝ[X]), ∀ x ∈ Set.Icc a b_1, |Polynomial.eval x p - f x| < ε

Tactic:
use p
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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) : 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

Premises used: ContinuousMap.norm_lt_iff
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 :
  ∀ (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 : ℝ) < ε
x : ℝ
m : x ∈ Set.Icc a b_1
⊢ |Polynomial.eval x p - f x| < ε

Tactic:
b ⟨x, m⟩

Premises used: Polynomial.eval, Subtype.mk
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
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 :
  ∀ (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 : ℝ) < ε
x : ℝ
m : x ∈ Set.Icc a b_1
⊢ |Polynomial.eval x p - f x| < ε

Tactic:
exact b ⟨x, m⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
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)
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
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
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)
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 }
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, zero_at_infty' := zero_at_infty' : α →C₀ β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
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 α β
toFun : α → β
continuous_toFun : Continuous[inst, inst_1] toFun
zero_at_infty' : Tendsto { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun (cocompact α) (𝓝 0)
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:
congr
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C₀ β
⊢ Eq (α := (a : α) → β) (⇑f.toContinuousMap : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f g : α →C₀ β
h : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α → β
hf : Continuous[inst, inst_1] f
hf' : Tendsto f (cocompact α) (𝓝 0)
⊢ (⇑{ toFun := f, continuous_toFun := hf, zero_at_infty' := hf' : α →C₀ β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
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 : α) → β)
rw : Continuous[inst, inst_1] (⇑f : (a : α) → β)
⊢ Continuous[inst, inst_1] f'

Tactic:
rw [h]