awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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]
-- 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
HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
⊢ 0 < M ^ (n - 1)

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_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)
rw : ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
⊢ ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)

Tactic:
rw [HH, le_div_iff₀ (by positivity)]

Premises used: le_div_iff₀
-- 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
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])
⊢ ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2

Tactic:
have hq (y : ℝ × ℝ) : IsMonicOfDegree (q y) 2 := isMonicOfDegree_sub_add_two ..
-- 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
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
simp :
  HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]) -
      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]) =
    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 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:
simp only [q]
-- 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
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
⊢ HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) w.1 : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) w.2 : ℝ[X]) -
      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]) =
    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:
ring
-- 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
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
⊢ 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
-- 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
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])
nth_rewrite : q w - (q w - q u) ∣ q w ^ n - (q w - q u) ^ n
⊢ q u ∣ q w ^ n - (q w - q u) ^ n

Tactic:
nth_rewrite 1 [← sub_sub_self (q w) (q u)]

Premises used: sub_sub_self
-- 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
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 w - (q w - q u) ∣ q w ^ n - (q w - q u) ^ n

Tactic:
sub_dvd_pow_sub_pow ..

Premises used: sub_dvd_pow_sub_pow
-- 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
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 w - (q w - q u) ∣ q w ^ n - (q w - q u) ^ n

Tactic:
exact sub_dvd_pow_sub_pow ..

Premises used: sub_dvd_pow_sub_pow
-- 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
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

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 ..
-- 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
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
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
⊢ ((q w - q u) ^ n).natDegree < 2 * n

Tactic:
rw [hsub]
-- 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
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
hbc : n < 2 * 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

Tactic:
compute_degree
-- 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
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
⊢ n < 2 * n

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

Tactic:
have H' : ((q w - q u) ^ n).natDegree < 2 * n := by rw [hsub]; compute_degree; grind
-- 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
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
⊢ 2 ≤ 2 * n

Tactic:
grind
-- 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
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
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
⊢ ‖φ 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

Premises used: Polynomial.IsMonicOfDegree.pow, Polynomial.IsMonicOfDegree.of_dvd_sub
-- 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
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
⊢ 2 * n - 2 = 2 * (n - 1)

Tactic:
grind
-- 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
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
⊢ p.IsMonicOfDegree (2 * (n - 1))

Tactic:
rw [show 2 * n - 2 = 2 * (n - 1) by grind] at hp
-- 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
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
hp₁ : p.IsMonicOfDegree (2 * (n - 1))
⊢ q w ^ n = p * q u + (q w - q u) ^ n

Tactic:
rw [show 2 * n - 2 = 2 * (n - 1) by grind] at hp
-- 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
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
grw : ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
grw [le_aeval_of_isMonicOfDegree hM₀.le (isMinOn_univ_iff.mp h) hp]

Premises used: LT.lt.le, _private.0.NormedAlgebra.Real.le_aeval_of_isMonicOfDegree, Iff.mp, isMinOn_univ_iff
-- 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
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
⊢ q u * p = q w ^ n - (q w - q u) ^ n

Tactic:
rw [← sub_eq_iff_eq_add, eq_comm, mul_comm] at hrel

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

Premises used: Norm.norm, Polynomial.aeval, DFunLike.coe
-- 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
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 :
  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)
⊢ ‖φ x u‖ * norm (E := F) ((aeval x : (a : ℝ[X]) → F) p : F) =
    ‖HSub.hSub (α := F) (β := F) ((aeval x : (a : ℝ[X]) → F) (q w ^ n) : F)
        ((aeval x : (a : ℝ[X]) → F) ((q w - q u) ^ n) : F)‖

Tactic:
rw [map_mul, norm_mul, map_sub, aeval_eq_φ x u] at hrel

Premises used: map_sub, norm_mul, map_mul, _private.0.NormedAlgebra.Real.aeval_eq_φ