awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
have H' (y : F) : aeval y (X + C r) = y + algebraMap ℂ F r := by simp
-- 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₂
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)
⊢ M ^ (n + 1) ≤
    norm (E := F) ((aeval (HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)) : (a : ℂ[X]) → F) p : F)

Tactic:
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 _)

Premises used: sub_add, map_sub, pow_succ, HSub.hSub, norm_mul, Polynomial.aeval_mul, mul_le_mul, mul_comm, norm_nonneg
-- 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)‖
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)
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)
⊢ M ^ n ≤ 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 _)

Premises used: sub_add, map_sub, pow_succ, norm_mul, Polynomial.aeval_mul, Polynomial.isMonicOfDegree_zero_iff, Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_mul_isMonicOfDegree, Iff.mp, mul_comm, 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
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 : ℂ
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
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)‖ =
    ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖

Tactic:
set M := ‖x - algebraMap ℂ F z‖ with hMdef

Premises used: Algebra.algebraMap, Complex, DFunLike.coe
-- 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
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) z : F)‖ ≠ 0

Tactic:
have := H z
-- 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
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)‖
this : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0
⊢ 0 < M

Tactic:
positivity
-- 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
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

Tactic:
have hM₀ : 0 < M := by have := H z; positivity
-- 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
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
⊢ Continuous.{0, u_1} (Y := F) fun (x_1 : ℂ) ↦ HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) x_1 : F)

Tactic:
fun_prop
-- 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
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
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)
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) c : F)‖ = M

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

Premises used: Eq.symm, _private.0.NormedAlgebra.norm_eq_of_isMinOn_of_forall_le
-- 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
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 : 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
dsimp :
  ‖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)
⊢ 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:
dsimp only at hy ⊢
-- 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
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
⊢ M * (1 + (‖w - y‖ / M) ^ n) = (M ^ n + ‖w - y‖ ^ n) / M ^ (n - 1)

Tactic:
simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn]

Premises used: Nat.sub_add_cancel, div_pow, pow_succ'
-- 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
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
⊢ 0 < M ^ (n - 1)

Tactic:
positivity
-- 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
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
rw : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ * M ^ (n - 1) ≤ M ^ n + ‖w - y‖ ^ n
⊢ ‖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)

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)]

Premises used: map_sub, NormOneClass.norm_one, norm_algebraMap, norm_sub_rev, mul_one, le_div_iff₀, sub_sub_sub_cancel_left
-- 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
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
⊢ 1 ≤ n

Tactic:
grind
-- 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
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
hbc₁ : 0 < n
⊢ (HPow.hPow (α := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (w - y) : ℂ[X]) n).natDegree < n

Tactic:
compute_degree!
-- 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
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
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
⊢ ‖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

Premises used: Polynomial.isMonicOfDegree_X_sub_one, HSub.hSub, Complex, Polynomial.X, sub_dvd_pow_sub_pow, Polynomial.isMonicOfDegree_X_pow, Polynomial.IsMonicOfDegree.of_dvd_sub
-- 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
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
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
⊢ ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) w : F)‖ * M ^ (n - 1) ≤ M ^ n + ‖w - y‖ ^ n

Tactic:
grw [le_aeval_of_isMonicOfDegree x hM₀.le (isMinOn_univ_iff.mp hz) hp y]

Premises used: LT.lt.le, Iff.mp, isMinOn_univ_iff, _private.0.NormedAlgebra.Complex.le_aeval_of_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
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 (α := ℂ[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

Premises used: eq_sub_iff_add_eq, eq_comm, mul_comm
-- 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
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
⊢ 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

Premises used: Norm.norm, Algebra.algebraMap, HSub.hSub, Polynomial.aeval, Complex, DFunLike.coe
-- 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
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) =
    ‖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

Premises used: sub_sub_sub_cancel_right, map_sub, norm_mul, map_pow, map_mul, Polynomial.aeval_C, Polynomial.aeval_X
-- 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
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‖
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
⊢ ‖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:
rw [hrel]
-- 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
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) 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:
simp [hy, ← map_sub]

Premises used: map_sub