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
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
y : ℝ × ℝ
hy : y ∈ SProd.sprod (α := Set ℝ) (β := Set ℝ) {0}ᶜ Set.univ
⊢ ‖y.1 • x - HSMul.hSMul (β := F) (y.1 * (y.1⁻¹ * y.2)) 1‖ = ‖y.1 • x - HSMul.hSMul (β := F) y.2 1‖

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
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
y : ℝ × ℝ
hy : y ∈ SProd.sprod (α := Set ℝ) (β := Set ℝ) {0}ᶜ Set.univ
calc : ‖y.1‖ * c ≤ ‖y.1‖ * ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖
calc₁ :
  ‖y.1‖ * ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) (y.1⁻¹ * y.2) : F)‖ =
    ‖HSub.hSub (β := F) (y.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) y.2 : F)‖
⊢ ‖y.1‖ * c ≤ ‖HSub.hSub (β := F) (y.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) y.2 : F)‖

Tactic:
calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all

Premises used: Real, HMul.hMul, Algebra.algebraMap, Prod.fst, Inv.inv, Prod.snd, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
refine_2 : Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖HSub.hSub (β := F) (x_1.1 • x) ((algebraMap ℝ F : (a : ℝ) → F) x_1.2 : F)‖)
    (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop

Tactic:
suffices Tendsto (fun y : ℝ × ℝ ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop by
      refine tendsto_atTop_mono' _ ?_ this
      filter_upwards [prod_mem_prod (isBounded_singleton (x := 0)) univ_mem] with y hy
      calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
refine_2 : Tendsto Prod.fst (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) (cobounded ℝ)
⊢ Tendsto (β := ℝ) (fun (y : ℝ × ℝ) ↦ ‖y.1‖ * c) (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) atTop

Tactic:
rw [tendsto_mul_const_atTop_of_pos hc₀, tendsto_norm_atTop_iff_cobounded]

Premises used: Filter.tendsto_mul_const_atTop_of_pos, tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
⊢ Tendsto Prod.fst (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) (cobounded ℝ)

Tactic:
tendsto_fst

Premises used: Filter.tendsto_fst
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
⊢ Tendsto Prod.fst (SProd.sprod (β := Filter ℝ) (cobounded ℝ) ⊤) (cobounded ℝ)

Tactic:
exact tendsto_fst

Premises used: Filter.tendsto_fst
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
obtain :
  ∀ (u : ℝ)
    (hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u),
    ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z

Tactic:
obtain ⟨u, hu⟩ := exists_isMinOn_norm_sub_smul ℝ x

Premises used: Real, NormedAlgebra.exists_isMinOn_norm_sub_smul
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
inl :
  ∀ (hc₀ : 0 = ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖),
    ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
inr :
  ∀ (hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖),
    ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z

Tactic:
rcases eq_or_lt_of_le (norm_nonneg (x - algebraMap ℝ F u)) with hc₀ | hc₀

Premises used: Real, Algebra.algebraMap, HSub.hSub, eq_or_lt_of_le, DFunLike.coe, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
hc₀ : 0 = ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
⊢ x = (algebraMap ℝ F : (a : ℝ) → F) u

Tactic:
rw [eq_comm, norm_eq_zero, sub_eq_zero] at hc₀

Premises used: norm_eq_zero, sub_eq_zero, eq_comm
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_2 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_2 : F)‖) univ u
hc₀ : x = (algebraMap ℝ F : (a : ℝ) → F) u
x_1 : ℝ × ℝ
⊢ Membership.mem (γ := Set (ℝ × ℝ)) univ x_1 →
    Membership.mem (γ := Set (ℝ × ℝ))
      {x_2 : ℝ × ℝ |
        (fun (x_3 : ℝ × ℝ) ↦
            LE.le (α := ℝ) ((fun (x_4 : ℝ × ℝ) ↦ ‖φ x x_4‖) (u, 0)) ((fun (x_4 : ℝ × ℝ) ↦ ‖φ x x_4‖) x_3))
          x_2}
      x_1

Tactic:
simp [φ, hc₀, sq, Algebra.smul_def]

Premises used: sq, _private.0.NormedAlgebra.Real.φ, 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
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
hc₀ : x = (algebraMap ℝ F : (a : ℝ) → F) u
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z

Tactic:
exact ⟨(u, 0), fun _ ↦ by simp [φ, hc₀, sq, 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
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
inr :
  ∀
    (hu :
      ∀ (x_1 : ℝ),
        ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖ ≤
          ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖),
    ∃ (z : ℝ × ℝ), ∀ (x_1 : ℝ × ℝ), ‖φ x z‖ ≤ ‖φ x x_1‖
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z

Tactic:
simp only [isMinOn_univ_iff] at hu ⊢

Premises used: 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
x : F
u : ℝ
hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
hu :
  ∀ (x_1 : ℝ),
    ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖ ≤
      ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖
⊢ ∃ (z : ℝ × ℝ), ∀ (x_1 : ℝ × ℝ), ‖φ x z‖ ≤ ‖φ x x_1‖

Tactic:
(continuous_φ x).norm.exists_forall_le_of_isBounded (0, 0) ?_

Premises used: _private.0.NormedAlgebra.Real.continuous_φ, Prod.mk, Continuous.exists_forall_le_of_isBounded, Continuous.norm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
hu :
  ∀ (x_1 : ℝ),
    ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖ ≤
      ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖
inr : Bornology.IsBounded (α := ℝ × ℝ) {x_1 : ℝ × ℝ | ‖φ x x_1‖ ≤ ‖φ x (0, 0)‖}
⊢ ∃ (z : ℝ × ℝ), ∀ (x_1 : ℝ × ℝ), ‖φ x z‖ ≤ ‖φ x x_1‖

Tactic:
refine (continuous_φ x).norm.exists_forall_le_of_isBounded (0, 0) ?_

Premises used: _private.0.NormedAlgebra.Real.continuous_φ, Prod.mk, Continuous.exists_forall_le_of_isBounded, Continuous.norm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
hu :
  ∀ (x_1 : ℝ),
    ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖ ≤
      ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖
⊢ Bornology.IsBounded (α := ℝ × ℝ) {x_1 : ℝ × ℝ | ‖φ x x_1‖ ≤ ‖φ x (0, 0)‖}

Tactic:
simpa [isBounded_def, compl_setOf, Ioi]
    using tendsto_norm_cobounded_atTop.comp (tendsto_φ_cobounded hc₀ hu) (Ioi_mem_atTop _)

Premises used: Set.Ioi, Bornology.isBounded_def, Filter.Ioi_mem_atTop, tendsto_norm_cobounded_atTop, _private.0.NormedAlgebra.Real.tendsto_φ_cobounded, Filter.Tendsto.comp, Set.compl_setOf
-- 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
obtain :
  ∀ (z : ℝ × ℝ) (h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z),
    ∃ (p : ℝ[X]), p.IsMonicOfDegree 2 ∧ Eq (α := F) ((aeval x : (a : ℝ[X]) → F) p : F) (0 : F)
⊢ ∃ (p : ℝ[X]), p.IsMonicOfDegree 2 ∧ Eq (α := F) ((aeval x : (a : ℝ[X]) → F) p : F) (0 : F)

Tactic:
obtain ⟨z, h⟩ := exists_isMinOn_norm_φ x

Premises used: _private.0.NormedAlgebra.Real.exists_isMinOn_norm_φ
-- 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
this rwa rwa₁ rwa₂ rwa₃ : φ x z = 0
⊢ Eq (α := F)
    ((aeval x : (a : ℝ[X]) → F)
        (HAdd.hAdd (β := ℝ[X])
          (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) z.1 : ℝ[X]) X)
          ((C : (a : ℝ) → ℝ[X]) z.2 : ℝ[X])) :
      F)
    (0 : F)

Tactic:
rwa [aeval_eq_φ]

Premises used: _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
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
suffices : φ x z = 0
⊢ ∃ (p : ℝ[X]), p.IsMonicOfDegree 2 ∧ Eq (α := F) ((aeval x : (a : ℝ[X]) → F) p : F) (0 : F)

Tactic:
suffices φ x z = 0 from ⟨_, isMonicOfDegree_sub_add_two z.1 z.2, by rwa [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
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
by_contra! : ∀ (H : φ x z ≠ 0), False
⊢ φ x z = 0

Tactic:
by_contra! H
-- 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
M : ℝ := ‖φ x z‖
r : ℝ
rw :
  ‖φ x z‖ ≤
    ‖HPow.hPow (β := ℕ) x 2 - HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) +
        HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2‖
⊢ √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖

Tactic:
rw [← sq_le_sq₀ M.sqrt_nonneg (norm_nonneg _), Real.sq_sqrt (norm_nonneg _), ← norm_pow,
      Commute.sub_sq <| algebraMap_eq_smul_one (A := F) r ▸ commute_algebraMap_right r x]

Premises used: norm_pow, Commute.sub_sq, Real.sq_sqrt, sq_le_sq₀, Real.sqrt_nonneg, 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
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ ‖φ x z‖ ≤ ‖φ x (2 * r, HPow.hPow (β := ℕ) r 2)‖

Tactic:
isMinOn_univ_iff.mp h (2 * r, r ^ 2)

Premises used: HMul.hMul, Prod.mk, HPow.hPow, Iff.mp, isMinOn_univ_iff, OfNat.ofNat
-- 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
M : ℝ := ‖φ x z‖
r : ℝ
h₁ : HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) = (2 * r, HPow.hPow (β := ℕ) r 2).1 • x
h₂ :
  HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2 =
    (algebraMap ℝ F : (a : ℝ) → F) (2 * r, HPow.hPow (β := ℕ) r 2).2
⊢ ‖φ x z‖ ≤
    ‖HPow.hPow (β := ℕ) x 2 - HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) +
        HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2‖

Tactic:
convert! isMinOn_univ_iff.mp h (2 * r, r ^ 2) using 4

Premises used: HMul.hMul, Prod.mk, HPow.hPow, Iff.mp, isMinOn_univ_iff, OfNat.ofNat
-- 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
M : ℝ := ‖φ x z‖
r : ℝ
⊢ HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) = (2 * r, HPow.hPow (β := ℕ) r 2).1 • x

Tactic:
simp [two_mul, add_mul, ← commutes, smul_def, mul_add]

Premises used: add_mul, two_mul, Algebra.smul_def, mul_add, Algebra.commutes
-- 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
M : ℝ := ‖φ x z‖
r : ℝ
⊢ HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2 =
    (algebraMap ℝ F : (a : ℝ) → F) (2 * r, HPow.hPow (β := ℕ) r 2).2

Tactic:
simp [two_mul, add_mul, ← commutes, smul_def, mul_add]

Premises used: add_mul, two_mul, Algebra.smul_def, mul_add, Algebra.commutes
-- 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
M : ℝ := ‖φ x z‖
⊢ ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖

Tactic:
have h' (r : ℝ) : √M ≤ ‖x - algebraMap ℝ F r‖ := by
    rw [← sq_le_sq₀ M.sqrt_nonneg (norm_nonneg _), Real.sq_sqrt (norm_nonneg _), ← norm_pow,
      Commute.sub_sq <| algebraMap_eq_smul_one (A := F) r ▸ commute_algebraMap_right r x]
    convert! isMinOn_univ_iff.mp h (2 * r, r ^ 2) using 4 <;>
      simp [two_mul, add_mul, ← commutes, smul_def, mul_add]
-- 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
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
⊢ 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
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
⊢ Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop

Tactic:
have := tendsto_norm_atTop_iff_cobounded.mpr <| tendsto_φ_cobounded (by positivity) h'
-- 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
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
⊢ Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x z‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop

Tactic:
simp only [norm_φ_eq_norm_φ_of_isMinOn h (norm_ne_zero_iff.mpr H)] at this

Premises used: Iff.mpr, norm_ne_zero_iff, _private.0.NormedAlgebra.Real.norm_φ_eq_norm_φ_of_isMinOn
-- 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
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x z‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
⊢ False

Tactic:
Filter.not_tendsto_const_atTop _ _ this

Premises used: Filter.not_tendsto_const_atTop
-- 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
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x z‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
⊢ False

Tactic:
exact Filter.not_tendsto_const_atTop _ _ this

Premises used: Filter.not_tendsto_const_atTop
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
⊢ Algebra.IsAlgebraic ℝ F

Tactic:
⟨fun x ↦ ?_⟩

Premises used: Algebra.IsAlgebraic.mk
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
refine : ∀ (x : F), IsAlgebraic ℝ x
⊢ Algebra.IsAlgebraic ℝ F

Tactic:
refine ⟨fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
x : F
obtain :
  ∀ (f : ℝ[X]) (hf : f.IsMonicOfDegree 2) (hfx : Eq (α := F) ((aeval x : (a : ℝ[X]) → F) f : F) (0 : F)),
    IsAlgebraic ℝ x
⊢ IsAlgebraic ℝ x

Tactic:
obtain ⟨f, hf, hfx⟩ := exists_isMonicOfDegree_two_and_aeval_eq_zero x

Premises used: NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
x : F
f : ℝ[X]
hf : f.IsMonicOfDegree 2
hfx : Eq (α := F) ((aeval x : (a : ℝ[X]) → F) f : F) (0 : F)
⊢ IsAlgebraic ℝ x

Tactic:
⟨f, hf.ne_zero, hfx⟩

Premises used: IsAlgebraic, And.intro, Polynomial.IsMonicOfDegree.ne_zero, Exists.intro
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
x : F
f : ℝ[X]
hf : f.IsMonicOfDegree 2
hfx : Eq (α := F) ((aeval x : (a : ℝ[X]) → F) f : F) (0 : F)
⊢ IsAlgebraic ℝ x

Tactic:
exact ⟨f, hf.ne_zero, hfx⟩
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
⊢ Algebra.IsAlgebraic ℝ F

Tactic:
have : Algebra.IsAlgebraic ℝ F := by
    refine ⟨fun x ↦ ?_⟩
    obtain ⟨f, hf, hfx⟩ := exists_isMonicOfDegree_two_and_aeval_eq_zero x
    exact ⟨f, hf.ne_zero, hfx⟩
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
this : Algebra.IsAlgebraic ℝ F
⊢ Nonempty.{max 1 (u_2 + 1)} (F ≃ₐ[ℝ] ℝ) ∨ Nonempty.{max 1 (u_2 + 1)} (F ≃ₐ[ℝ] ℂ)

Tactic:
_root_.Real.nonempty_algEquiv_or F

Premises used: Real.nonempty_algEquiv_or
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
this : Algebra.IsAlgebraic ℝ F
⊢ Nonempty.{max 1 (u_2 + 1)} (F ≃ₐ[ℝ] ℝ) ∨ Nonempty.{max 1 (u_2 + 1)} (F ≃ₐ[ℝ] ℂ)

Tactic:
exact _root_.Real.nonempty_algEquiv_or F

Premises used: Real.nonempty_algEquiv_or
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Ring 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : T2Space 𝔸
inst_6 : Algebra ℚ 𝔸
v : m → 𝔸
simp_rw :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (diagonal v ^ n))
    (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
simp_rw₁ :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (diagonal (v ^ n)))
    (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
simp_rw₂ :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), diagonal (HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
    (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
⊢ exp (diagonal v) = diagonal (exp v)

Tactic:
simp_rw [exp_eq_tsum_rat, diagonal_pow, ← diagonal_smul, ← diagonal_tsum]

Premises used: Matrix.diagonal_pow, Matrix.diagonal_smul, NormedSpace.exp_eq_tsum_rat, Matrix.diagonal_tsum
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
n : Type u_2
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Ring 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
inst_7 : T2Space 𝔸
inst_8 : Algebra ℚ 𝔸
v : m → Matrix n n 𝔸
simp_rw :
  Eq (α := Matrix (n × m) (n × m) 𝔸) (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (blockDiagonal v ^ n_1))
    (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
simp_rw₁ :
  Eq (α := Matrix (n × m) (n × m) 𝔸)
    (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (blockDiagonal (v ^ n_1)))
    (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
simp_rw₂ :
  Eq (α := Matrix (n × m) (n × m) 𝔸)
    (∑' (n_1 : ℕ), blockDiagonal (HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
    (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
⊢ exp (blockDiagonal v) = blockDiagonal (exp v)

Tactic:
simp_rw [exp_eq_tsum_rat, ← blockDiagonal_pow, ← blockDiagonal_smul, ← blockDiagonal_tsum]

Premises used: Matrix.blockDiagonal_tsum, Matrix.blockDiagonal_smul, Matrix.blockDiagonal_pow, NormedSpace.exp_eq_tsum_rat