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 : 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)‖
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)‖ = M
have hM₀ : 0 < M
Tactic: have hM₀ : 0 < M := by have := H z; positivity
-- 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 : ℂ
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)‖ = M
have refine : ∀ {y : ℂ} (w : ℂ)
  (hy : norm.{u_1} (E := F) ((fun (x_1 : ℂ) ↦ HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)) y) = M)
  (n : ℕ) (hn : n > 0),
  norm.{u_1} (E := F) ((fun (x_1 : ℂ) ↦ HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)) w) ≤
    M *
      (1 +
        (‖HSub.hSub (α := F) ((fun (x_1 : ℂ) ↦ HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)) w)
                ((fun (x_1 : ℂ) ↦ HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)) y)‖ /
            M) ^
          n)
Tactic: refine norm_eq_of_isMinOn_of_forall_le (f := (x - algebraMap ℂ F ·)) hM₀ hMdef.symm hz
    (by fun_prop) (fun {y} w hy n hn ↦ ?_) c
-- 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 : ℂ
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ ≤
    M *
      (1 +
        (‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F) -
                HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ /
            M) ^
          n)
have rw : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ * M ^ (n - 1) ≤ M ^ n + ‖w - y‖ ^ n
Tactic: rw [sub_sub_sub_cancel_left, ← map_sub, norm_algebraMap, norm_sub_rev y w, norm_one, mul_one,
    show M * (1 + (‖w - y‖ / M) ^ n) = (M ^ n + ‖w - y‖ ^ n) / M ^ (n - 1) by
      simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn],
    le_div_iff₀ (by positivity)]
-- 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 : ℂ
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
⊢ (HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n).natDegree < n
have hbc : n * 0 < n
Tactic: compute_degree!
-- 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 : ℂ
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
hbc : n * 0 < n
⊢ (HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n).natDegree < n
have hbc₁ : 0 < n
Tactic: compute_degree!
-- 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 : ℂ
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ * M ^ (n - 1) ≤ M ^ n + ‖w - y‖ ^ n
have obtain : ∀ (p : ℂ[X]) (hp : p.IsMonicOfDegree (n - 1))
  (hrel :
    HPow.hPow (α := ℂ[X]) X n =
      p * HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) +
        HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n),
  ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ * M ^ (n - 1) ≤ M ^ n + ‖w - y‖ ^ n
Tactic: obtain ⟨p, hp, hrel⟩ :=
    (isMonicOfDegree_X_pow ℂ n).of_dvd_sub (by grind)
      (isMonicOfDegree_X_sub_one (w - y)) (by compute_degree!) <| sub_dvd_pow_sub_pow X _ n
-- 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 : ℂ
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hMdef : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel :
  HPow.hPow (α := ℂ[X]) X n =
    p * HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) +
      HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ * M ^ (n - 1) ≤ M ^ n + ‖w - y‖ ^ n
have grw : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ *
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F) p : F) ≤
  M ^ n + ‖w - y‖ ^ n
Tactic: grw [le_aeval_of_isMonicOfDegree x hM₀.le (isMinOn_univ_iff.mp hz) hp y]
-- 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)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel :
  HPow.hPow (α := ℂ[X]) X n =
    p * HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) +
      HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ *
      norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F) p : F) ≤
    M ^ n + ‖w - y‖ ^ n
have hrel₁ : HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) * p =
  HPow.hPow (α := ℂ[X]) X n - HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n
Tactic: rw [eq_comm, ← eq_sub_iff_add_eq, mul_comm] at hrel
Cleared hypotheses: hrel
-- 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)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel :
  HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) * p =
    HPow.hPow (α := ℂ[X]) X n - HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ *
      norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F) p : F) ≤
    M ^ n + ‖w - y‖ ^ n
have hrel₁ : norm (E := F)
    ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F)
        (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) * p) :
      F) =
  norm (E := F)
    ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F)
        (HPow.hPow (α := ℂ[X]) X n - HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n) :
      F)
Tactic: apply_fun (‖aeval (x - algebraMap ℂ F y) ·‖) at hrel
Cleared hypotheses: hrel
-- 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)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel :
  norm (E := F)
      ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F)
          (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) * p) :
        F) =
    norm (E := F)
      ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F)
          (HPow.hPow (α := ℂ[X]) X n - HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n) :
        F)
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ *
      norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F) p : F) ≤
    M ^ n + ‖w - y‖ ^ n
have hrel₁ : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ *
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F) p : F) =
  ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F) ^ n -
      HSub.hSub (α := F) (β := F) ((algebraMap ℂ F : (a : ℂ) → F) w : F) ((algebraMap ℂ F : (a : ℂ) → F) y : F) ^ n‖
Tactic: simp only [map_sub, map_mul, aeval_X, aeval_C, sub_sub_sub_cancel_right, norm_mul, map_pow]
    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 : 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)‖
hM₀ : 0 < M
y w : ℂ
hy : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel :
  ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ *
      norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F) p : F) =
    ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F) ^ n -
        HSub.hSub (α := F) (β := F) ((algebraMap ℂ F : (a : ℂ) → F) w : F) ((algebraMap ℂ F : (a : ℂ) → F) y : F) ^ n‖
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ *
      norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F)) : (a : ℂ[X]) → F) p : F) ≤
    M ^ n + ‖w - y‖ ^ n
have rw : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) y : F) ^ n -
      HSub.hSub (α := F) (β := F) ((algebraMap ℂ F : (a : ℂ) → F) w : F) ((algebraMap ℂ F : (a : ℂ) → F) y : F) ^ n‖ ≤
  M ^ n + ‖w - y‖ ^ n
Tactic: rw [hrel]
-- 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 : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
have obtain : ∀ (z : ℂ)
  (hz : IsMinOn (β := ℝ) (fun (x_1 : ℂ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)‖) Set.univ z),
  ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
Tactic: obtain ⟨z, hz⟩ := exists_isMinOn_norm_sub_smul ℂ x
-- 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)‖) Set.univ z
⊢ ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
have hM : let M := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖;
M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
Tactic: set M := ‖x - algebraMap ℂ F z‖ with hM
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
⊢ ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
have inl : ∀ (hM₀ : 0 = M), ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
Tactic: rcases eq_or_lt_of_le (show 0 ≤ M from norm_nonneg _) with hM₀ | hM₀
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
inl : ∀ (hM₀ : 0 = M), ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
⊢ ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
have inr : ∀ (hM₀ : 0 < M), ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
Tactic: rcases eq_or_lt_of_le (show 0 ≤ M from norm_nonneg _) with hM₀ | hM₀
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
⊢ ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
have inr : ∀ (H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0), False
Tactic: by_contra! 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
z : ℂ
hz : IsMinOn (β := ℝ) (fun (x_1 : ℂ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
⊢ False
have key : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F)‖ =
  ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
Tactic: have key := norm_sub_eq_norm_sub_of_isMinOn hz H (‖x‖ + M + 1)
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
key :
  ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F)‖ =
    ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
⊢ False
have key₁ : ‖HSub.hSub (α := F) ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F) x‖ = M
Tactic: rw [← hM, norm_sub_rev] at key
Cleared hypotheses: key
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
key : ‖HSub.hSub (α := F) ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F) x‖ = M
⊢ False
have key₁ : norm (E := F) ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F) - ‖x‖ ≤ M
Tactic: replace key := (norm_sub_norm_le ..).trans_eq key
Cleared hypotheses: key
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
key : norm (E := F) ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F) - ‖x‖ ≤ M
⊢ False
have key₁ : ‖(↑‖x‖ : ℂ) + (↑M : ℂ) + 1‖ - ‖x‖ ≤ M
Tactic: rw [norm_algebraMap, norm_one, mul_one] at key
Cleared hypotheses: key
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
key : ‖(↑‖x‖ : ℂ) + (↑M : ℂ) + 1‖ - ‖x‖ ≤ M
⊢ False
have key₁ : ‖‖x‖ + M + 1‖ - ‖x‖ ≤ M
Tactic: norm_cast at key
Cleared hypotheses: key
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
key : ‖‖x‖ + M + 1‖ - ‖x‖ ≤ M
⊢ False
have key₁ : ‖x‖ + M + 1 - ‖x‖ ≤ M
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)] at key
Cleared hypotheses: key
-- 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)‖) Set.univ z
M : ℝ := ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM : M = ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
key : ‖x‖ + M + 1 - ‖x‖ ≤ M
⊢ False
have linarith : -1 + (‖x‖ + M + 1 - ‖x‖ - M) = 0
Tactic: linarith only [key]
-- 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
inst_4 : Nontrivial F
⊢ Function.Bijective (α := ℂ) (β := F) (⇑(ofId ℂ F) : (a : ℂ) → F)
have refine : ∀ (x : F), ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x
Tactic: refine ⟨FaithfulSMul.algebraMap_injective ℂ F, fun x ↦ ?_⟩
-- 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
inst_4 : Nontrivial F
x : F
⊢ ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x
have obtain : ∀ (z : ℂ) (hz : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0),
  ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x
Tactic: obtain ⟨z, hz⟩ := exists_norm_sub_smul_one_eq_zero x
-- 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
inst_4 : Nontrivial F
x : F
z : ℂ
hz : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
⊢ ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x
have refine : (ofId ℂ F : (a : ℂ) → F) z = x
Tactic: refine ⟨z, ?_⟩