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
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:
exact (norm_sub_le ..).trans <| by simp [hy, ← map_sub]

Premises used: norm_sub_le, LE.le.trans
-- 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
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
⊢ ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0

Tactic:
obtain ⟨z, hz⟩ := exists_isMinOn_norm_sub_smul ℂ x

Premises used: NormedAlgebra.exists_isMinOn_norm_sub_smul, Complex
-- 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)‖) Set.univ z
⊢ 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

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)‖) 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
inr : ∀ (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

Tactic:
rcases eq_or_lt_of_le (show 0 ≤ M from norm_nonneg _) with hM₀ | hM₀

Premises used: Algebra.algebraMap, HSub.hSub, eq_or_lt_of_le, Complex, DFunLike.coe, 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
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

Tactic:
⟨z, hM₀.symm⟩

Premises used: Exists.intro, Eq.symm
-- 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)‖) 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

Tactic:
exact ⟨z, hM₀.symm⟩
-- 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)‖) 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
inr : ∀ (H : ∀ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ ≠ 0), False
⊢ ∃ (z : ℂ), ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0

Tactic:
by_contra! H
-- 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)‖) 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
⊢ ‖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)
-- 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)‖) 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)‖
⊢ ‖HSub.hSub (α := F) ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F) x‖ = M

Tactic:
rw [← hM, norm_sub_rev] at key

Premises used: norm_sub_rev
-- 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)‖) 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
⊢ norm (E := F) ((algebraMap ℂ F : (a : ℂ) → F) ((↑‖x‖ : ℂ) + (↑M : ℂ) + 1) : F) - ‖x‖ ≤ M

Tactic:
replace key := (norm_sub_norm_le ..).trans_eq key
-- 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)‖) 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
⊢ ‖(↑‖x‖ : ℂ) + (↑M : ℂ) + 1‖ - ‖x‖ ≤ M

Tactic:
rw [norm_algebraMap, norm_one, mul_one] at key

Premises used: NormOneClass.norm_one, norm_algebraMap, mul_one
-- 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)‖) 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
⊢ ‖‖x‖ + M + 1‖ - ‖x‖ ≤ M

Tactic:
norm_cast at key
-- 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)‖) 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
⊢ 0 ≤ ‖x‖ + M + 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)‖) 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
⊢ ‖x‖ + M + 1 - ‖x‖ ≤ M

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)] at key

Premises used: abs_of_nonneg, Real.norm_eq_abs
-- 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)‖) 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
linarith : -1 + (‖x‖ + M + 1 - ‖x‖ - M) = 0
⊢ False

Tactic:
linarith only [key]
-- 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
inst_4 : Nontrivial F
⊢ Function.Bijective (α := ℂ) (β := F) (⇑(ofId ℂ F) : (a : ℂ) → F)

Tactic:
⟨FaithfulSMul.algebraMap_injective ℂ F, fun x ↦ ?_⟩

Premises used: FaithfulSMul.algebraMap_injective, And.intro, Function.Bijective, Complex
-- 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
inst_4 : Nontrivial F
refine : ∀ (x : F), ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x
⊢ Function.Bijective (α := ℂ) (β := F) (⇑(ofId ℂ F) : (a : ℂ) → F)

Tactic:
refine ⟨FaithfulSMul.algebraMap_injective ℂ F, fun 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
inst_4 : Nontrivial F
x : F
obtain :
  ∀ (z : ℂ) (hz : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0),
    ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x
⊢ ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x

Tactic:
obtain ⟨z, hz⟩ := exists_norm_sub_smul_one_eq_zero x

Premises used: NormedAlgebra.Complex.exists_norm_sub_smul_one_eq_zero
-- 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
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

Tactic:
⟨z, ?_⟩

Premises used: Exists.intro
-- 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
inst_4 : Nontrivial F
x : F
z : ℂ
hz : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
refine : (ofId ℂ F : (a : ℂ) → F) z = x
⊢ ∃ (a : ℂ), (ofId ℂ F : (a : ℂ) → F) a = x

Tactic:
refine ⟨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
inst_4 : Nontrivial F
x : F
z : ℂ
hz : ‖HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F)‖ = 0
rwa : ∀ (hz : HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F) = 0), (ofId ℂ F : (a : ℂ) → F) z = x
rwa₁ : ∀ (hz : x = (algebraMap ℂ F : (a : ℂ) → F) z), (ofId ℂ F : (a : ℂ) → F) z = x
rwa₂ : ∀ (hz : (algebraMap ℂ F : (a : ℂ) → F) z = x), (ofId ℂ F : (a : ℂ) → F) z = x
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hz : (ofId ℂ F : (a : ℂ) → F) z = x), (ofId ℂ F : (a : ℂ) → F) z = x
⊢ (ofId ℂ F : (a : ℂ) → F) z = x

Tactic:
rwa [norm_eq_zero, sub_eq_zero, eq_comm, ← ofId_apply] at hz

Premises used: norm_eq_zero, sub_eq_zero, eq_comm, Algebra.ofId_apply
-- 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
inst_4 : Nontrivial F
⊢ Nonempty.{max (u_1 + 1) 1} (ℂ ≃ₐ[ℂ] F)

Tactic:
⟨algEquivOfNormMul F⟩

Premises used: NormedAlgebra.Complex.algEquivOfNormMul, Nonempty.intro
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
x : F
⊢ Continuous (φ x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
x : F
u : ℝ × ℝ
⊢ (aeval x : (a : ℝ[X]) → F)
      (HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])) =
    φ x u

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
p : ℝ[X]
hp : p.IsMonicOfDegree (HMul.hMul (α := ℕ) 2 0)
⊢ HPow.hPow (β := ℕ) M 0 ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (2 * n)), M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n + 1))
⊢ p.IsMonicOfDegree (2 * n + 2)

Tactic:
rw [mul_add, mul_one] at hp

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

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

Premises used: Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_two_mul_isMonicOfDegree
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (2 * n)), M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
succ :
  ∀ (a b : ℝ)
    (hab :
      f₁ =
        HAdd.hAdd (β := ℝ[X])
          (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) a : ℝ[X]) X)
          ((C : (a : ℝ) → ℝ[X]) b : ℝ[X])),
    M ^ (n + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
⊢ M ^ (n + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)

Tactic:
obtain ⟨a, b, hab⟩ := isMonicOfDegree_two_iff'.mp hf₁

Premises used: Polynomial.isMonicOfDegree_two_iff', Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (2 * n)), M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
a b : ℝ
hab :
  f₁ =
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) a : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) b : ℝ[X])
succ : M ^ n * M ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) f₂ : F) * ‖φ x (a, b)‖
⊢ M ^ (n + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)

Tactic:
rw [H, aeval_mul, norm_mul, mul_comm, pow_succ, hab, aeval_eq_φ x (a, b)]

Premises used: pow_succ, Prod.mk, norm_mul, Polynomial.aeval_mul, mul_comm, _private.0.NormedAlgebra.Real.aeval_eq_φ
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (2 * n)), M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
a b : ℝ
hab :
  f₁ =
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) a : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) b : ℝ[X])
⊢ M ^ n * M ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) f₂ : F) * ‖φ x (a, b)‖

Tactic:
mul_le_mul (ih hf₂) (h (a, b)) hM (norm_nonneg _)

Premises used: Prod.mk, mul_le_mul, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (2 * n)), M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
a b : ℝ
hab :
  f₁ =
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) a : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) b : ℝ[X])
⊢ M ^ n * M ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) f₂ : F) * ‖φ x (a, b)‖

Tactic:
exact mul_le_mul (ih hf₂) (h (a, b)) hM (norm_nonneg _)

Premises used: Prod.mk, mul_le_mul, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
p : ℝ[X]
n : ℕ
hp : p.IsMonicOfDegree (2 * n)
zero :
  ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (HMul.hMul (α := ℕ) 2 0)),
    HPow.hPow (β := ℕ) M 0 ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
succ :
  ∀ (n : ℕ)
    (ih : ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (2 * n)), M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F))
    {p : ℝ[X]} (hp : p.IsMonicOfDegree (2 * (n + 1))), M ^ (n + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
⊢ M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)

Tactic:
induction n generalizing p with
  | zero => simp_all
  | succ n ih =>
    rw [mul_add, mul_one] at hp
    obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_two_mul_isMonicOfDegree
    obtain ⟨a, b, hab⟩ := isMonicOfDegree_two_iff'.mp hf₁
    rw [H, aeval_mul, norm_mul, mul_comm, pow_succ, hab, aeval_eq_φ x (a, b)]
    exact mul_le_mul (ih hf₂) (h (a, b)) hM (norm_nonneg _)

Premises used: pow_succ, norm_mul, Polynomial.aeval_mul, Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_two_mul_isMonicOfDegree, mul_comm, mul_add, mul_one
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : ‖φ x z‖ ≠ 0
w : ℝ × ℝ
set :
  let M := ‖φ x z‖;
  ∀ (H : M ≠ 0) (hM : M = ‖φ x z‖), ‖φ x w‖ = M
⊢ ‖φ x w‖ = ‖φ x z‖

Tactic:
set M : ℝ := ‖φ x z‖ with hM

Premises used: _private.0.NormedAlgebra.Real.φ
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
⊢ 0 < M

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
⊢ 0 < M

Tactic:
have hM₀ : 0 < M := by positivity
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
⊢ ‖φ x w‖ = M

Tactic:
norm_eq_of_isMinOn_of_forall_le hM₀ hM.symm h (continuous_φ x) (fun {w} u hw n hn ↦ ?_) w

Premises used: _private.0.NormedAlgebra.Real.continuous_φ, 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 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
refine :
  ∀ {w : ℝ × ℝ} (u : ℝ × ℝ) (hw : ‖φ x w‖ = M) (n : ℕ) (hn : n > 0), ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)
⊢ ‖φ x w‖ = M

Tactic:
refine norm_eq_of_isMinOn_of_forall_le hM₀ hM.symm h (continuous_φ x) (fun {w} u hw n hn ↦ ?_) w

Premises used: _private.0.NormedAlgebra.Real.continuous_φ, 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 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
w_1 : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
⊢ M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ 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'