awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (ofId ℂ F : (a : ℂ) → F) z = x
have rwa : ∀ (hz : HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F) = 0), (ofId ℂ F : (a : ℂ) → F) z = x
Tactic: rwa [norm_eq_zero, sub_eq_zero, eq_comm, ← ofId_apply] at hz
Cleared hypotheses: hz
-- 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
rwa : ∀ (hz : HSub.hSub (β := F) x ((algebraMap ℂ F : (a : ℂ) → F) z : F) = 0), (ofId ℂ F : (a : ℂ) → F) z = x
⊢ (ofId ℂ F : (a : ℂ) → F) z = x
have rwa₁ : ∀ (hz : x = (algebraMap ℂ F : (a : ℂ) → F) z), (ofId ℂ F : (a : ℂ) → F) z = x
Tactic: rwa [norm_eq_zero, sub_eq_zero, eq_comm, ← ofId_apply] at hz
Cleared hypotheses: hz
-- 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
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
⊢ (ofId ℂ F : (a : ℂ) → F) z = x
have rwa₂ : ∀ (hz : (algebraMap ℂ 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
Cleared hypotheses: hz
-- 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
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
⊢ (ofId ℂ F : (a : ℂ) → F) z = x
have rwa₃ : ∀ (hz : (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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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))
⊢ M ^ (n + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
have hp₁ : p.IsMonicOfDegree (2 * n + 2)
Tactic: rw [mul_add, mul_one] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)
⊢ M ^ (n + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
have 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)
Tactic: obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_two_mul_isMonicOfDegree
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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₂
⊢ M ^ (n + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
have 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)
Tactic: obtain ⟨a, b, hab⟩ := isMonicOfDegree_two_iff'.mp hf₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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 + 1) ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
have succ : M ^ n * M ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) f₂ : F) * ‖φ x (a, b)‖
Tactic: rw [H, aeval_mul, norm_mul, mul_comm, pow_succ, hab, aeval_eq_φ x (a, b)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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)
⊢ M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
have zero : ∀ {p : ℝ[X]} (hp : p.IsMonicOfDegree (HMul.hMul (α := ℕ) 2 0)),
  HPow.hPow (β := ℕ) M 0 ≤ 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 _)
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 : 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)
⊢ M ^ n ≤ norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F)
have 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)
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 _)
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 : 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 : ℝ × ℝ
⊢ ‖φ x w‖ = ‖φ x z‖
have set : let M := ‖φ x z‖;
∀ (H : M ≠ 0) (hM : M = ‖φ x z‖), ‖φ x w‖ = M
Tactic: set M : ℝ := ‖φ x z‖ with hM
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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‖
⊢ ‖φ x w‖ = M
have hM₀ : 0 < M
Tactic: have hM₀ : 0 < M := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
have refine : ∀ {w : ℝ × ℝ} (u : ℝ × ℝ) (hw : ‖φ x w‖ = M) (n : ℕ) (hn : n > 0), ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)
Tactic: refine norm_eq_of_isMinOn_of_forall_le hM₀ hM.symm h (continuous_φ x) (fun {w} u hw n hn ↦ ?_) w
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
⊢ ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)
have HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
Tactic: have HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1) := by
    simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
⊢ ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)
have rw : ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Tactic: rw [HH, le_div_iff₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
Tactic: have hq (y : ℝ × ℝ) : IsMonicOfDegree (q y) 2 := isMonicOfDegree_sub_add_two ..
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have hsub : q w - q u =
  HSub.hSub (β := ℝ[X])
    (HAdd.hAdd (β := ℝ[X])
      (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
      ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
    ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])
Tactic: have hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2 := by simp only [q]; ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub :
  q w - q u =
    HSub.hSub (β := ℝ[X])
      (HAdd.hAdd (β := ℝ[X])
        (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
      ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])
⊢ q u ∣ q w ^ n - (q w - q u) ^ n
have nth_rewrite : q w - (q w - q u) ∣ q w ^ n - (q w - q u) ^ n
Tactic: nth_rewrite 1 [← sub_sub_self (q w) (q u)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub :
  q w - q u =
    HSub.hSub (β := ℝ[X])
      (HAdd.hAdd (β := ℝ[X])
        (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
      ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
Tactic: have hdvd : q u ∣ q w ^ n - (q w - q u) ^ n := by
    nth_rewrite 1 [← sub_sub_self (q w) (q u)]
    exact sub_dvd_pow_sub_pow ..
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub :
  q w - q u =
    HSub.hSub (β := ℝ[X])
      (HAdd.hAdd (β := ℝ[X])
        (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
      ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ ((q w - q u) ^ n).natDegree < 2 * n
have rw : (HSub.hSub (β := ℝ[X])
        (HAdd.hAdd (β := ℝ[X])
          (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
          ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
        ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X]) ^
      n).natDegree <
  2 * n
Tactic: rw [hsub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub :
  q w - q u =
    HSub.hSub (β := ℝ[X])
      (HAdd.hAdd (β := ℝ[X])
        (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
      ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ (HSub.hSub (β := ℝ[X])
          (HAdd.hAdd (β := ℝ[X])
            (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
            ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
          ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X]) ^
        n).natDegree <
    2 * n
have hbc : n < 2 * n
Tactic: compute_degree
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub :
  q w - q u =
    HSub.hSub (β := ℝ[X])
      (HAdd.hAdd (β := ℝ[X])
        (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
      ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have H' : ((q w - q u) ^ n).natDegree < 2 * n
Tactic: have H' : ((q w - q u) ^ n).natDegree < 2 * n := by rw [hsub]; compute_degree; grind
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub :
  q w - q u =
    HSub.hSub (β := ℝ[X])
      (HAdd.hAdd (β := ℝ[X])
        (HSub.hSub (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) u.1 : ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) * X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]))
      ((C : (a : ℝ) → ℝ[X]) u.2 : ℝ[X])
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
H' : ((q w - q u) ^ n).natDegree < 2 * n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have obtain : ∀ (p : ℝ[X]) (hp : p.IsMonicOfDegree (2 * n - 2)) (hrel : q w ^ n = p * q u + (q w - q u) ^ n),
  ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Tactic: obtain ⟨p, hp, hrel⟩ := ((hq w).pow n).of_dvd_sub (by grind) (hq u) H' hdvd
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n - 2)
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have hp₁ : p.IsMonicOfDegree (2 * (n - 1))
Tactic: rw [show 2 * n - 2 = 2 * (n - 1) by grind] at hp
Cleared hypotheses: hp, hrel
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have grw : ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Tactic: grw [le_aeval_of_isMonicOfDegree hM₀.le (isMinOn_univ_iff.mp h) hp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have hrel₁ : q u * p = q w ^ n - (q w - q u) ^ n
Tactic: rw [← sub_eq_iff_eq_add, eq_comm, 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 : 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
q : (y : ℝ × ℝ) → ℝ[X] :=
  fun (y : ℝ × ℝ) ↦
    HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) y.1 : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) y.2 : ℝ[X])
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : q u * p = q w ^ n - (q w - q u) ^ n
⊢ ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
have hrel₁ : norm (E := F) ((aeval x : (a : ℝ[X]) → F) (q u * p) : F) =
  norm (E := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n - (q w - q u) ^ n) : F)
Tactic: apply_fun (‖aeval x ·‖) at hrel
Cleared hypotheses: hrel