awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop
have suffices : (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
Tactic: suffices h : (r : ℝ≥0∞) ≤ p.radius by
    convert! h
    simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]
    congr
    ext n
    rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]
    exact fun ha => (lt_self_iff_false _).mp
      (ha.2.trans_le (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ)))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
⊢ (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
have H₁ : HasFPowerSeriesOnBall.{0, 0, u_2} (F := A) (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ)
  (cauchyPowerSeries (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ) 0 (↑r : ℝ)) 0 (↑r : ℝ≥0∞)
Tactic: have H₁ := (differentiableOn_inverse_one_sub_smul r_lt).hasFPowerSeriesOnBall r_pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
⊢ Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (‖a ^ n‖ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) atTop (𝓝 (spectralRadius ℂ a))
have h : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (‖a ^ n‖ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) fun (n : ℕ) ↦
  (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: convert! pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (‖a ^ n‖ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) fun (n : ℕ) ↦
    (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have h : ∀ (x : ℕ), ENNReal.ofReal (‖a ^ x‖ ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)) = (↑‖a ^ x‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
x : ℕ
⊢ ENNReal.ofReal (‖a ^ x‖ ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)) = (↑‖a ^ x‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
have rw : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
Tactic: rw [← ofReal_rpow_of_nonneg (norm_nonneg _) _, ← coe_nnnorm, coe_nnreal_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
⊢ (spectrum ℂ a).Nonempty
have by_contra! : ∀ (h : spectrum ℂ a = ∅), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
⊢ resolventSet ℂ a = Set.univ
have rwa : ∀ (h : (resolventSet ℂ a)ᶜ = ∅), resolventSet ℂ a = Set.univ
Tactic: rwa [spectrum, Set.compl_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
rwa : ∀ (h : (resolventSet ℂ a)ᶜ = ∅), resolventSet ℂ a = Set.univ
⊢ resolventSet ℂ a = Set.univ
have rwa₁ : ∀ (h : resolventSet ℂ a = Set.univ), resolventSet ℂ a = Set.univ
Tactic: rwa [spectrum, Set.compl_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
⊢ False
have H₀ : resolventSet ℂ a = Set.univ
Tactic: have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
⊢ False
have H₁ : Differentiable.{0, 0, u_2} ℂ (F := A) fun (z : ℂ) ↦ resolvent a z
Tactic: have H₁ : Differentiable ℂ fun z : ℂ => resolvent a z := fun z =>
    hasDerivAt_resolvent_const_left (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)
      |>.differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable.{0, 0, u_2} ℂ (F := A) fun (z : ℂ) ↦ resolvent a z
⊢ False
have H₃ : resolvent (R := ℂ) a 0 = 0
Tactic: have H₃ := H₁.apply_eq_of_tendsto_cocompact 0 <| by
    simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
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
⊢ (algebraMap ℂ A : (a : ℂ) → A) z = a
have rwa : ∀ (h : ¬IsUnit (HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a)), (algebraMap ℂ A : (a : ℂ) → A) z = a
Tactic: rwa [mem_iff, hA, Classical.not_not, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
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
⊢ (algebraMap ℂ A : (a : ℂ) → A) z = a
have rwa₁ : ∀ (h : ¬HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a ≠ 0), (algebraMap ℂ A : (a : ℂ) → A) z = a
Tactic: rwa [mem_iff, hA, Classical.not_not, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
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
⊢ (algebraMap ℂ A : (a : ℂ) → A) z = a
have rwa₂ : ∀ (h : HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a = 0), (algebraMap ℂ A : (a : ℂ) → A) z = a
Tactic: rwa [mem_iff, hA, Classical.not_not, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
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
⊢ (algebraMap ℂ A : (a : ℂ) → A) z = a
have rwa₃ : ∀ (h : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ‖f y‖ = M
have suffices : Eq.{u_1 + 1} (α := Set X) {y : X | ‖f y‖ = M} univ
Tactic: suffices {y | ‖f y‖ = M} = univ by simpa only [← this, hx] using mem_univ y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ Eq.{u_1 + 1} (α := Set X) {y : X | ‖f y‖ = M} univ
have refine : IsOpen[inst] {y : X | ‖f y‖ = M}
Tactic: refine IsClopen.eq_univ ⟨isClosed_eq (by fun_prop) (by fun_prop), ?_⟩ <| nonempty_of_mem hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ IsOpen[inst] {y : X | ‖f y‖ = M}
have 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
Tactic: rw [isOpen_iff_eventually]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ∀ᶠ (y : X) in 𝓝 w, Membership.mem (γ := Set X) {y : X | ‖f y‖ = M} y
have h₁ : ∀ (u : X) (hu : u ∈ f ⁻¹' Metric.ball (f w) M), ‖f u‖ = M
Tactic: filter_upwards [mem_map.mp <| hf.tendsto w (Metric.ball_mem_nhds (f w) hM)] with u hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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‖ = M
have hu₁ : ‖f u - f w‖ / M < 1
Tactic: simp only [mem_preimage, Metric.mem_ball, dist_eq_norm, ← div_lt_one₀ hM] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
have h₁ : ‖f u‖ ≤ M
Tactic: refine le_antisymm ?_ (hx ▸ isMinOn_univ_iff.mp h u)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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))
⊢ ‖f u‖ ≤ M
have refine : ∀ᶠ (c : ℕ) in atTop, ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ c)
Tactic: refine ge_of_tendsto (by simpa) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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))
⊢ ∀ᶠ (c : ℕ) in atTop, ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ c)
have h₁ : ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) (Ioi 0) n), ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ n)
Tactic: filter_upwards [Ioi_mem_atTop 0] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
have h₁ : Tendsto (fun (n : ℕ) ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * HAdd.hAdd (α := ℝ) 1 0))
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
⊢ ∃ (z : 𝕜), IsMinOn (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) univ z
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ∃ (z : 𝕜), IsMinOn (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖) univ z
have 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)‖
Tactic: simp only [isMinOn_univ_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
⊢ ∃ (z : 𝕜),
    ∀ (x_1 : 𝕜),
      ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) z : F)‖ ≤
        ‖HSub.hSub (β := F) x ((algebraMap 𝕜 F : (a : 𝕜) → F) x_1 : F)‖
have 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)‖}
Tactic: refine (show Continuous fun z : 𝕜 ↦ ‖x - algebraMap 𝕜 F z‖ by fun_prop)
    |>.exists_forall_le_of_isBounded 0 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)
⊢ M ^ (n + 1) ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
have 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)
Tactic: obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_one_mul_isMonicOfDegree
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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₂
⊢ M ^ (n + 1) ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
have 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)
Tactic: obtain ⟨r, rfl⟩ := isMonicOfDegree_one_iff.mp hf₁
Cleared hypotheses: f₁, hf₁, H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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₂
⊢ M ^ (n + 1) ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
have H' : ∀ (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: have H' (y : F) : aeval y (X + C r) = y + algebraMap ℂ F r := by simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)‖
p : ℂ[X]
n : ℕ
hp : p.IsMonicOfDegree n
c : ℂ
⊢ M ^ n ≤ norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
have zero : ∀ {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: induction n generalizing p with
  | zero => simp [isMonicOfDegree_zero_iff.mp hp]
  | succ n ih =>
    obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_one_mul_isMonicOfDegree
    obtain ⟨r, rfl⟩ := isMonicOfDegree_one_iff.mp hf₁
    have H' (y : F) : aeval y (X + C r) = y + algebraMap ℂ F r := by simp
    simpa only [pow_succ, mul_comm, H, aeval_mul, H', sub_add, ← map_sub, norm_mul]
      using mul_le_mul (ih hf₂) (h (c - r)) hM (norm_nonneg _)
Cleared hypotheses: p, n, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)‖
p : ℂ[X]
n : ℕ
hp : p.IsMonicOfDegree n
c : ℂ
zero :
  ∀ {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)
⊢ M ^ n ≤ norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
have succ : ∀ (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)),
  M ^ (n + 1) ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)
Tactic: induction n generalizing p with
  | zero => simp [isMonicOfDegree_zero_iff.mp hp]
  | succ n ih =>
    obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_one_mul_isMonicOfDegree
    obtain ⟨r, rfl⟩ := isMonicOfDegree_one_iff.mp hf₁
    have H' (y : F) : aeval y (X + C r) = y + algebraMap ℂ F r := by simp
    simpa only [pow_succ, mul_comm, H, aeval_mul, H', sub_add, ← map_sub, norm_mul]
      using mul_le_mul (ih hf₂) (h (c - r)) hM (norm_nonneg _)
Cleared hypotheses: p, n, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
inst_3 : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (β := ℝ) (fun (x_1 : ℂ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)‖) univ z
H : ∀ (z' : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z' : F)‖ ≠ 0
c : ℂ
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)‖ =
    ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
have set : let M := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖;
∀ (hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖),
  ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)‖ = M
Tactic: set M := ‖x - algebraMap ℂ F z‖ with hMdef
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
inst_3 : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (β := ℝ) (fun (x_1 : ℂ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)‖) univ z
H : ∀ (z' : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z' : F)‖ ≠ 0
c : ℂ
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
⊢ 0 < M
have this : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
Tactic: have := H z