awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
⊢ ∃ z ∈ spectrum ℂ a, (↑‖z‖₊ : ℝ≥0∞) = spectralRadius ℂ a

Tactic:
exists_nnnorm_eq_spectralRadius_of_nonempty (spectrum.nonempty a)

Premises used: Set.Mem, spectrum.nonempty, spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
r : ℝ≥0
hr : ∀ z ∈ spectrum ℂ a, ‖z‖₊ < r
⊢ spectralRadius ℂ a < (↑r : ℝ≥0∞)

Tactic:
spectralRadius_lt_of_forall_lt_of_nonempty (spectrum.nonempty a) hr

Premises used: spectrum.spectralRadius_lt_of_forall_lt_of_nonempty, spectrum.nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
p : ℂ[X]
⊢ spectrum ℂ (A := A) ((aeval a : (a : ℂ[X]) → A) p : A) = (fun (k : ℂ) ↦ eval k p) '' spectrum ℂ a

Tactic:
map_polynomial_aeval_of_nonempty a p (spectrum.nonempty a)

Premises used: spectrum.nonempty, spectrum.map_polynomial_aeval_of_nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
n : ℕ
⊢ spectrum ℂ (a ^ n) = (fun (x : ℂ) ↦ x ^ n) '' spectrum ℂ a

Tactic:
simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval a (X ^ n)

Premises used: Polynomial.aeval_X_pow, Polynomial.eval_X_pow, HPow.hPow, Polynomial.X, spectrum.map_polynomial_aeval
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0
a : A
z : ℂ
h : z ∈ spectrum ℂ a
rwa :
  ∀ (h : ¬IsUnit (HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a)), (algebraMap ℂ A : (a : ℂ) → A) z = a
rwa₁ : ∀ (h : ¬HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a ≠ 0), (algebraMap ℂ A : (a : ℂ) → A) z = a
rwa₂ : ∀ (h : HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a = 0), (algebraMap ℂ A : (a : ℂ) → A) z = a
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : (algebraMap ℂ A : (a : ℂ) → A) z = a), (algebraMap ℂ A : (a : ℂ) → A) z = a
⊢ (algebraMap ℂ A : (a : ℂ) → A) z = a

Tactic:
rwa [mem_iff, hA, Classical.not_not, sub_eq_zero] at h

Premises used: Classical.not_not, sub_eq_zero, spectrum.mem_iff
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0
nt : Nontrivial A := ⋯
z : ℂ
⊢ (fun (a : A) ↦ Set.Nonempty.some (s := spectrum ℂ a) ⋯) ((algebraMap ℂ A : (a : ℂ) → A) z) = z

Tactic:
simpa only [@scalar_eq _ _ _ _ _ nt _] using
        (@spectrum.nonempty _ _ _ _ nt <| algebraMap ℂ A z).some_mem

Premises used: Algebra.algebraMap, Set.Nonempty.some_mem, spectrum.nonempty, spectrum.scalar_eq, Complex, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
this : Eq.{u_1 + 1} (α := Set X) {y : X | ‖f y‖ = M} univ
⊢ ‖f y‖ = M

Tactic:
simpa only [← this, hx] using mem_univ y

Premises used: Set.mem_univ
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
suffices : Eq.{u_1 + 1} (α := Set X) {y : X | ‖f y‖ = M} univ
⊢ ‖f y‖ = M

Tactic:
suffices {y | ‖f y‖ = M} = univ by simpa only [← this, hx] using mem_univ y
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
⊢ Continuous[inst, _] fun (y : X) ↦ ‖f y‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
⊢ Continuous[inst, _] fun (y : X) ↦ M

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
refine : IsOpen[inst] {y : X | ‖f y‖ = M}
⊢ Eq.{u_1 + 1} (α := Set X) {y : X | ‖f y‖ = M} univ

Tactic:
refine IsClopen.eq_univ ⟨isClosed_eq (by fun_prop) (by fun_prop), ?_⟩ <| nonempty_of_mem hx

Premises used: IsClopen.eq_univ, isClosed_eq, And.intro, Set.nonempty_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
rw :
  ∀ (x : X),
    Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} x →
      ∀ᶠ (y : X) in 𝓝 x, Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} y
⊢ IsOpen[inst] {y : X | ‖f y‖ = M}

Tactic:
rw [isOpen_iff_eventually]

Premises used: isOpen_iff_eventually
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
h₁ : ∀ (u : X) (hu : u ∈ f ⁻¹' Metric.ball (f w) M), ‖f u‖ = M
⊢ ∀ᶠ (y : X) in 𝓝 w, Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} y

Tactic:
filter_upwards [mem_map.mp <| hf.tendsto w (Metric.ball_mem_nhds (f w) hM)] with u hu

Premises used: Continuous.tendsto, Metric.ball_mem_nhds, Iff.mp, Filter.mem_map
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : u ∈ f ⁻¹' Metric.ball (f w) M
⊢ ‖f u - f w‖ / M < 1

Tactic:
simp only [mem_preimage, Metric.mem_ball, dist_eq_norm, ← div_lt_one₀ hM] at hu

Premises used: dist_eq_norm, Metric.mem_ball, div_lt_one₀, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
⊢ ‖f u‖ = M

Tactic:
le_antisymm ?_ (hx ▸ isMinOn_univ_iff.mp h u)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
h₁ : ‖f u‖ ≤ M
⊢ ‖f u‖ = M

Tactic:
refine le_antisymm ?_ (hx ▸ isMinOn_univ_iff.mp h u)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))
⊢ Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 M)

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))
refine : ∀ᶠ (c : ℕ) in atTop, ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ c)
⊢ ‖f u‖ ≤ M

Tactic:
refine ge_of_tendsto (by simpa) ?_

Premises used: ge_of_tendsto
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))
h₁ : ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) (Ioi 0) n), ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ n)
⊢ ∀ᶠ (c : ℕ) in atTop, ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ c)

Tactic:
filter_upwards [Ioi_mem_atTop 0] with n hn

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))
n : ℕ
hn : Membership.mem (γ := Set ℕ) (Ioi 0) n
⊢ ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ n)

Tactic:
H u hw n hn
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))
n : ℕ
hn : Membership.mem (γ := Set ℕ) (Ioi 0) n
⊢ ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ n)

Tactic:
exact H u hw n hn
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
h₁ : Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))
⊢ ‖f u‖ ≤ M

Tactic:
suffices Tendsto (fun n : ℕ ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * (1 + 0))) by
    refine ge_of_tendsto (by simpa) ?_
    filter_upwards [Ioi_mem_atTop 0] with n hn
    exact H u hw n hn
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
⊢ 0 ≤ ‖f u - f w‖ / M

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (β := ℝ) (fun (x : X) ↦ ‖f x‖) univ x
hf : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} w
u : X
hu : ‖f u - f w‖ / M < 1
⊢ Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one (by positivity) hu |>.const_add 1 |>.const_mul M

Premises used: Filter.Tendsto.const_mul, tendsto_pow_atTop_nhds_zero_of_lt_one, Filter.Tendsto.const_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : SeminormedRing F
inst_3 : NormedAlgebra 𝕜 F
inst_4 : NormOneClass F
x : F
⊢ Tendsto (⇑(algebraMap 𝕜 F) : (a : 𝕜) → F) (cobounded 𝕜) (cobounded F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : SeminormedRing F
inst_3 : NormedAlgebra 𝕜 F
inst_4 : NormOneClass F
x : F
⊢ Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) (cobounded 𝕜) atTop

Tactic:
exact tendsto_norm_cobounded_atTop |>.comp <| tendsto_const_sub_cobounded x |>.comp <| by simp

Premises used: tendsto_const_sub_cobounded, tendsto_norm_cobounded_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : SeminormedRing F
inst_3 : NormedAlgebra 𝕜 F
inst_4 : NormOneClass F
x : F
⊢ Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) (cobounded 𝕜) atTop

Tactic:
have : Tendsto (‖x - algebraMap 𝕜 F ·‖) (cobounded 𝕜) atTop := by
    exact tendsto_norm_cobounded_atTop |>.comp <| tendsto_const_sub_cobounded x |>.comp <| by simp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : SeminormedRing F
inst_3 : NormedAlgebra 𝕜 F
inst_4 : NormOneClass F
x : F
this :
  Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) (cobounded 𝕜) atTop
simp :
  ∃ (z : 𝕜),
    ∀ (x_1 : 𝕜),
      ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) z : F)‖ ≤
        ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖
⊢ ∃ (z : 𝕜), IsMinOn (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) univ z

Tactic:
simp only [isMinOn_univ_iff]

Premises used: isMinOn_univ_iff
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : SeminormedRing F
inst_3 : NormedAlgebra 𝕜 F
inst_4 : NormOneClass F
x : F
this :
  Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) (cobounded 𝕜) atTop
⊢ Continuous (Y := ℝ) fun (z : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) z : F)‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : SeminormedRing F
inst_3 : NormedAlgebra 𝕜 F
inst_4 : NormOneClass F
x : F
this :
  Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) (cobounded 𝕜) atTop
refine :
  Bornology.IsBounded.{u_1} (α := 𝕜)
    {x_1 : 𝕜 |
      ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖ ≤
        ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) 0 : F)‖}
⊢ ∃ (z : 𝕜),
    ∀ (x_1 : 𝕜),
      ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) z : F)‖ ≤
        ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖

Tactic:
refine (show Continuous fun z : 𝕜 ↦ ‖x - algebraMap 𝕜 F z‖ by fun_prop)
    |>.exists_forall_le_of_isBounded 0 ?_

Premises used: Continuous.exists_forall_le_of_isBounded, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : SeminormedRing F
inst_3 : NormedAlgebra 𝕜 F
inst_4 : NormOneClass F
x : F
this :
  Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) (cobounded 𝕜) atTop
⊢ Bornology.IsBounded.{u_1} (α := 𝕜)
    {x_1 : 𝕜 |
      ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖ ≤
        ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) 0 : F)‖}

Tactic:
simpa [isBounded_def, compl_setOf, Ioi] using this (Ioi_mem_atTop ‖x - (0 : 𝕜) • 1‖)

Premises used: Norm.norm, Set.Ioi, HSub.hSub, Bornology.isBounded_def, Filter.Ioi_mem_atTop, HSMul.hSMul, OfNat.ofNat, Set.compl_setOf
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
inst_3 : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z' : F)‖
c : ℂ
p : ℂ[X]
hp : p.IsMonicOfDegree 0
⊢ HPow.hPow (β := ℕ) M 0 ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)

Tactic:
simp [isMonicOfDegree_zero_iff.mp hp]

Premises used: Polynomial.isMonicOfDegree_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
inst_3 : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z' : F)‖
c : ℂ
n : ℕ
ih :
  ∀ {p : ℂ[X]} (hp : p.IsMonicOfDegree n),
    M ^ n ≤ norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
p : ℂ[X]
hp : p.IsMonicOfDegree (n + 1)
succ :
  ∀ (f₁ f₂ : ℂ[X]) (hf₁ : f₁.IsMonicOfDegree 1) (hf₂ : f₂.IsMonicOfDegree n) (H : p = f₁ * f₂),
    M ^ (n + 1) ≤
      norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
⊢ M ^ (n + 1) ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)

Tactic:
obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_one_mul_isMonicOfDegree

Premises used: Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_mul_isMonicOfDegree
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
inst_3 : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z' : F)‖
c : ℂ
n : ℕ
ih :
  ∀ {p : ℂ[X]} (hp : p.IsMonicOfDegree n),
    M ^ n ≤ norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
p : ℂ[X]
hp : p.IsMonicOfDegree (n + 1)
f₁ f₂ : ℂ[X]
hf₁ : f₁.IsMonicOfDegree 1
hf₂ : f₂.IsMonicOfDegree n
H : p = f₁ * f₂
succ :
  ∀ (r : ℂ) (hf₁ : (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X])).IsMonicOfDegree 1)
    (H : p = HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) * f₂),
    M ^ (n + 1) ≤
      norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
⊢ M ^ (n + 1) ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)

Tactic:
obtain ⟨r, rfl⟩ := isMonicOfDegree_one_iff.mp hf₁

Premises used: Polynomial.isMonicOfDegree_one_iff, Iff.mp, rfl
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
inst_3 : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z' : F)‖
c : ℂ
n : ℕ
ih :
  ∀ {p : ℂ[X]} (hp : p.IsMonicOfDegree n),
    M ^ n ≤ norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
p : ℂ[X]
hp : p.IsMonicOfDegree (n + 1)
f₂ : ℂ[X]
hf₂ : f₂.IsMonicOfDegree n
r : ℂ
hf₁ : (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X])).IsMonicOfDegree 1
H : p = HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X]) * f₂
y : F
⊢ (aeval y : (a : ℂ[X]) → F) (HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) r : ℂ[X])) =
    HAdd.hAdd (β := F) y ((algebraMap ℂ F : (a : ℂ) → F) r : F)

Tactic:
simp