awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w_1 : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel :
  ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) =
    ‖HSub.hSub (α := F) (β := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n) : F)
        ((aeval x : (a : ℝ[X]) → F) ((q w - q u) ^ n) : F)‖
rw :
  ‖HSub.hSub (α := F) (β := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n) : F)
        ((aeval x : (a : ℝ[X]) → F) ((q w - q u) ^ n) : F)‖ ≤
    M ^ n + ‖φ x w - φ x u‖ ^ n
⊢ ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
rw [hrel, norm_sub_rev (φ ..)]

Premises used: _private.0.NormedAlgebra.Real.φ, norm_sub_rev
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w_1 : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel :
  ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) =
    ‖HSub.hSub (α := F) (β := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n) : F)
        ((aeval x : (a : ℝ[X]) → F) ((q w - q u) ^ n) : F)‖
⊢ norm (E := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n) : F) +
      norm (E := F) ((aeval x : (a : ℝ[X]) → F) ((q w - q u) ^ n) : F) ≤
    M ^ n + ‖φ x w - φ x u‖ ^ n

Tactic:
simp [q, aeval_eq_φ, hw]

Premises used: _private.0.NormedAlgebra.Real.aeval_eq_φ
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w_1 : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel :
  ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) =
    ‖HSub.hSub (α := F) (β := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n) : F)
        ((aeval x : (a : ℝ[X]) → F) ((q w - q u) ^ n) : F)‖
⊢ ‖HSub.hSub (α := F) (β := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n) : F)
        ((aeval x : (a : ℝ[X]) → F) ((q w - q u) ^ n) : F)‖ ≤
    M ^ n + ‖φ x w - φ x u‖ ^ n

Tactic:
exact (norm_sub_le ..).trans <| by simp [q, aeval_eq_φ, hw]

Premises used: norm_sub_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
simp_rw :
  Tendsto
    (fun (x_1 : ℝ × ℝ) ↦
      HPow.hPow (β := ℕ) x 2 - HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F))
    (cobounded (ℝ × ℝ)) (cobounded F)
⊢ Tendsto (fun (x_1 : ℝ × ℝ) ↦ φ x x_1) (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
simp_rw [φ, sub_add]

Premises used: sub_add, _private.0.NormedAlgebra.Real.φ
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
⊢ Tendsto
    (fun (x_1 : ℝ × ℝ) ↦
      HPow.hPow (β := ℕ) x 2 - HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F))
    (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
tendsto_const_sub_cobounded _ |>.comp ?_

Premises used: tendsto_const_sub_cobounded, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
refine :
  Tendsto (fun (x_1 : ℝ × ℝ) ↦ HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F))
    (cobounded (ℝ × ℝ)) (cobounded F)
⊢ Tendsto
    (fun (x_1 : ℝ × ℝ) ↦
      HPow.hPow (β := ℕ) x 2 - HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F))
    (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
refine tendsto_const_sub_cobounded _ |>.comp ?_

Premises used: tendsto_const_sub_cobounded, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
rw :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (cobounded (ℝ × ℝ)) atTop
⊢ Tendsto (fun (x_1 : ℝ × ℝ) ↦ HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F))
    (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
rw [← tendsto_norm_atTop_iff_cobounded]

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (cobounded (ℝ × ℝ)) atTop

Tactic:
Tendsto.coprod_of_prod_top_right (α := ℝ) (fun s hs ↦ ?_) ?_

Premises used: Filter.Tendsto.coprod_of_prod_top_right
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
refine_1 :
  ∀ (s : Set ℝ) (hs : s ∈ cobounded ℝ),
    Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
      (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
refine_2 :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (cobounded (ℝ × ℝ)) atTop

Tactic:
refine Tendsto.coprod_of_prod_top_right (α := ℝ) (fun s hs ↦ ?_) ?_

Premises used: Filter.Tendsto.coprod_of_prod_top_right
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : s ∈ cobounded ℝ
⊢ Bornology.IsBounded sᶜ

Tactic:
rw [← isCobounded_def, ← isBounded_compl_iff] at hs

Premises used: Bornology.isBounded_compl_iff, Bornology.isCobounded_def
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
⊢ ∃ M > 0, ∀ y ∈ sᶜ, ‖y‖ ≤ M

Tactic:
hs.exists_pos_norm_le

Premises used: Bornology.IsBounded.exists_pos_norm_le
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
refine_1 :
  ∀ (M : ℝ) (hM_pos : M > 0) (hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M),
    Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
      (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

Tactic:
obtain ⟨M, hM_pos, hM⟩ : ∃ M > 0, ∀ y ∈ sᶜ, ‖y‖ ≤ M := hs.exists_pos_norm_le

Premises used: Bornology.IsBounded.exists_pos_norm_le
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

Tactic:
tendsto_atTop_mono' _ ?_ this

Premises used: Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
refine :
  (𝓟 sᶜ ×ˢ cobounded ℝ).EventuallyLE (β := ℝ)
    (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖) fun (x_1 : ℝ × ℝ) ↦
    ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ this

Premises used: Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
h :
  ∀ (w : ℝ × ℝ) (hw : w ∈ SProd.sprod (β := Set ℝ) sᶜ Set.univ),
    norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - M * ‖x‖ ≤
      ‖HSub.hSub (β := F) (w.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F)‖
⊢ (𝓟 sᶜ ×ˢ cobounded ℝ).EventuallyLE (β := ℝ)
    (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖) fun (x_1 : ℝ × ℝ) ↦
    ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖

Tactic:
filter_upwards [prod_mem_prod (mem_principal_self sᶜ) univ_mem] with w hw

Premises used: Filter.mem_principal_self, Compl.compl, Filter.prod_mem_prod, Filter.univ_mem
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ SProd.sprod (β := Set ℝ) sᶜ Set.univ
h :
  norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - M * ‖x‖ ≤
    ‖HSub.hSub (α := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) (w.1 • x)‖
⊢ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - M * ‖x‖ ≤
    ‖HSub.hSub (β := F) (w.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F)‖

Tactic:
rw [norm_sub_rev]

Premises used: norm_sub_rev
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ SProd.sprod (β := Set ℝ) sᶜ Set.univ
⊢ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - M * ‖x‖ ≤
    ‖HSub.hSub (α := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) (w.1 • x)‖

Tactic:
le_trans ?_ (norm_sub_norm_le ..)

Premises used: norm_sub_norm_le, le_trans
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ SProd.sprod (β := Set ℝ) sᶜ Set.univ
h :
  norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - M * ‖x‖ ≤
    norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - ‖w.1 • x‖
⊢ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - M * ‖x‖ ≤
    ‖HSub.hSub (α := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) (w.1 • x)‖

Tactic:
refine le_trans ?_ (norm_sub_norm_le ..)

Premises used: norm_sub_norm_le, le_trans
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ SProd.sprod (β := Set ℝ) sᶜ Set.univ
⊢ ‖w.1‖ ≤ M

Tactic:
specialize hM _ (Set.mem_prod.mp hw).1

Premises used: Set.mem_prod, And.left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ SProd.sprod (β := Set ℝ) sᶜ Set.univ
hM : ‖w.1‖ ≤ M
h : ‖w.2‖ - M * ‖x‖ ≤ ‖w.2‖ - ‖w.1‖ * ‖x‖
⊢ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - M * ‖x‖ ≤
    norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - ‖w.1 • x‖

Tactic:
simp only [norm_algebraMap', norm_smul]

Premises used: norm_smul, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
this :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ SProd.sprod (β := Set ℝ) sᶜ Set.univ
hM : ‖w.1‖ ≤ M
h : 0 ≤ ‖x‖
⊢ ‖w.2‖ - M * ‖x‖ ≤ ‖w.2‖ - ‖w.1‖ * ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
refine_1 :
  Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

Tactic:
suffices Tendsto (‖algebraMap ℝ F ·.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop by
      refine tendsto_atTop_mono' _ ?_ this
      filter_upwards [prod_mem_prod (mem_principal_self sᶜ) univ_mem] with w hw
      rw [norm_sub_rev]
      refine le_trans ?_ (norm_sub_norm_le ..)
      specialize hM _ (Set.mem_prod.mp hw).1
      simp only [norm_algebraMap', norm_smul]
      gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
refine_1 : Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖x_1.2‖ + -(M * ‖x‖)) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

Tactic:
simp only [norm_algebraMap', sub_eq_add_neg]

Premises used: sub_eq_add_neg, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖x_1.2‖ + -(M * ‖x‖)) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

Tactic:
tendsto_atTop_add_const_right _ _ <| tendsto_norm_atTop_iff_cobounded.mpr tendsto_snd

Premises used: Filter.tendsto_atTop_add_const_right, Iff.mpr, tendsto_norm_atTop_iff_cobounded, Filter.tendsto_snd
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖x_1.2‖ + -(M * ‖x‖)) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

Tactic:
exact tendsto_atTop_add_const_right _ _ <| tendsto_norm_atTop_iff_cobounded.mpr tendsto_snd

Premises used: Filter.tendsto_atTop_add_const_right, Iff.mpr, tendsto_norm_atTop_iff_cobounded, Filter.tendsto_snd
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop

Tactic:
tendsto_atTop_mono' _ ?_ this

Premises used: Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
refine :
  (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤).EventuallyLE (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) fun (x_1 : ℝ × ℝ) ↦
    ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ this

Premises used: Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
h :
  ∀ (y : ℝ × ℝ) (hy : y ∈ SProd.sprod (α := Set ℝ) (β := Set ℝ) {0}ᶜ Set.univ),
    ‖y.1‖ * c ≤ ‖HSub.hSub (β := F) (y.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) y.2 : F)‖
⊢ (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤).EventuallyLE (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) fun (x_1 : ℝ × ℝ) ↦
    ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖

Tactic:
filter_upwards [prod_mem_prod (isBounded_singleton (x := 0)) univ_mem] with y hy

Premises used: Filter.prod_mem_prod, Filter.univ_mem, Bornology.isBounded_singleton
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
y : ℝ × ℝ
hy : y ∈ SProd.sprod (α := Set ℝ) (β := Set ℝ) {0}ᶜ Set.univ
hbc : c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖
⊢ ‖y.1‖ * c ≤ ‖y.1‖ * ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
y : ℝ × ℝ
hy : y ∈ SProd.sprod (α := Set ℝ) (β := Set ℝ) {0}ᶜ Set.univ
⊢ c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖

Tactic:
hbd _
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
y : ℝ × ℝ
hy : y ∈ SProd.sprod (α := Set ℝ) (β := Set ℝ) {0}ᶜ Set.univ
⊢ c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖

Tactic:
exact hbd _
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
y : ℝ × ℝ
hy : y ∈ SProd.sprod (α := Set ℝ) (β := Set ℝ) {0}ᶜ Set.univ
simp : ‖y.1 • x - HSMul.hSMul (β := F) (y.1 * (y.1⁻¹ * y.2)) 1‖ = ‖y.1 • x - HSMul.hSMul (β := F) y.2 1‖
⊢ ‖y.1‖ * ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖ =
    ‖HSub.hSub (β := F) (y.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) y.2 : F)‖

Tactic:
simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]

Premises used: norm_smul, smul_smul, Algebra.algebraMap_eq_smul_one, smul_sub