awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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 :
  norm (E := F) ((aeval x : (a : ℝ[X]) → F) (q u * p) : F) =
    norm (E := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n - (q w - q u) ^ n) : F)
⊢ ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have 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)‖
Tactic: rw [map_mul, norm_mul, map_sub, aeval_eq_φ x u] at hrel
Cleared hypotheses: hrel
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)‖
⊢ ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have 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
Tactic: rw [hrel, norm_sub_rev (φ ..)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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 : ℝ × ℝ) ↦ φ x x_1) (cobounded (ℝ × ℝ)) (cobounded F)
have 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)
Tactic: simp_rw [φ, sub_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)
have refine : Tendsto (fun (x_1 : ℝ × ℝ) ↦ 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 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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 (ℝ × ℝ)) (cobounded F)
have rw : Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
  (cobounded (ℝ × ℝ)) atTop
Tactic: rw [← tendsto_norm_atTop_iff_cobounded]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
have 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
Tactic: refine Tendsto.coprod_of_prod_top_right (α := ℝ) (fun s hs ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (cobounded (ℝ × ℝ)) atTop
have 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
Tactic: refine Tendsto.coprod_of_prod_top_right (α := ℝ) (fun s hs ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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 ℝ
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
have hs₁ : Bornology.IsBounded sᶜ
Tactic: rw [← isCobounded_def, ← isBounded_compl_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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ᶜ
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
have 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
Tactic: obtain ⟨M, hM_pos, hM⟩ : ∃ M > 0, ∀ y ∈ sᶜ, ‖y‖ ≤ M := hs.exists_pos_norm_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
have 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)‖
Tactic: refine tendsto_atTop_mono' _ ?_ this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ (𝓟 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)‖
have 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)‖
Tactic: filter_upwards [prod_mem_prod (mem_principal_self sᶜ) univ_mem] with w hw
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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) (w.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F)‖
have 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)‖
Tactic: rw [norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)‖
have 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‖
Tactic: refine le_trans ?_ (norm_sub_norm_le ..)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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‖ ≤
    norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) w.2 : F) - ‖w.1 • x‖
have hM₁ : ‖w.1‖ ≤ M
Tactic: specialize hM _ (Set.mem_prod.mp hw).1
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ 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‖
have h : ‖w.2‖ - M * ‖x‖ ≤ ‖w.2‖ - ‖w.1‖ * ‖x‖
Tactic: simp only [norm_algebraMap', norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ‖w.2‖ - M * ‖x‖ ≤ ‖w.2‖ - ‖w.1‖ * ‖x‖
have h : 0 ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
have refine_1 : Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
  (𝓟 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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 : ℝ × ℝ) ↦ norm (E := F) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F) - M * ‖x‖)
    (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
have refine_1 : Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖x_1.2‖ + -(M * ‖x‖)) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
Tactic: simp only [norm_algebraMap', sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
have 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)‖
Tactic: refine tendsto_atTop_mono' _ ?_ this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ (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)‖
have 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)‖
Tactic: filter_upwards [prod_mem_prod (isBounded_singleton (x := 0)) univ_mem] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ‖y.1‖ * c ≤ ‖y.1‖ * ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖
have hbc : c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ‖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)‖
have simp : ‖y.1 • x - HSMul.hSMul (β := F) (y.1 * (y.1⁻¹ * y.2)) 1‖ = ‖y.1 • x - HSMul.hSMul (β := F) y.2 1‖
Tactic: simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ‖y.1‖ * c ≤ ‖HSub.hSub (β := F) (y.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) y.2 : F)‖
have calc : ‖y.1‖ * c ≤ ‖y.1‖ * ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖
Tactic: calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
calc : ‖y.1‖ * c ≤ ‖y.1‖ * ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖
⊢ ‖y.1‖ * c ≤ ‖HSub.hSub (β := F) (y.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) y.2 : F)‖
have calc₁ : ‖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: calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)‖)
    (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
have refine_2 : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
Tactic: suffices Tendsto (fun y : ℝ × ℝ ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop by
      refine tendsto_atTop_mono' _ ?_ this
      filter_upwards [prod_mem_prod (isBounded_singleton (x := 0)) univ_mem] with y hy
      calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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 (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
have refine_2 : Tendsto Prod.fst (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) (cobounded ℝ)
Tactic: rw [tendsto_mul_const_atTop_of_pos hc₀, tendsto_norm_atTop_iff_cobounded]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
have obtain : ∀ (u : ℝ)
  (hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u),
  ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
Tactic: obtain ⟨u, hu⟩ := exists_isMinOn_norm_sub_smul ℝ x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
have inl : ∀ (hc₀ : 0 = ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖),
  ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
Tactic: rcases eq_or_lt_of_le (norm_nonneg (x - algebraMap ℝ F u)) with hc₀ | hc₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
inl :
  ∀ (hc₀ : 0 = ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖),
    ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
have inr : ∀ (hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖),
  ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
Tactic: rcases eq_or_lt_of_le (norm_nonneg (x - algebraMap ℝ F u)) with hc₀ | hc₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
hc₀ : 0 = ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
have hc₁ : x = (algebraMap ℝ F : (a : ℝ) → F) u
Tactic: rw [eq_comm, norm_eq_zero, sub_eq_zero] at hc₀
Cleared hypotheses: hc₀