mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Tactic:
·

Goal state after:
case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case refine_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z ↦ ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k ↦ (expSeries ℝ ℍ (2 * k)) fun x ↦ q) ↑c

pp: case refine_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z ↦ ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k ↦ (expSeries ℝ ℍ (2 * k + 1)) fun x ↦ q) ((s / ‖q‖) • q)

Tactic:
·

Goal state after:
case refine_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z ↦ ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k ↦ (expSeries ℝ ℍ (2 * k)) fun x ↦ q) ↑c
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case refine_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z ↦ ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k ↦ (expSeries ℝ ℍ (2 * k + 1)) fun x ↦ q) ((s / ‖q‖) • q)

Tactic:
·

Goal state after:
case refine_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z ↦ ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k ↦ (expSeries ℝ ℍ (2 * k + 1)) fun x ↦ q) ((s / ‖q‖) • q)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case e_a.inl
q : ℍ
hv : ‖q.im‖ = 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

pp: case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
·

Goal state after:
case e_a.inl
q : ℍ
hv : ‖q.im‖ = 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x : R
⊢ ‖x + 0‖ ≤ max ‖x‖ ‖0‖

pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x : R
⊢ ‖x + 0‖ ≤ max ‖x‖ ‖0‖
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ max ‖x‖ 1
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ max ‖x‖ 1
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case refine_1
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : s ∈ cobounded ℝ
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

pp: case refine_2
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (cobounded ℝ ×ˢ ⊤) atTop

Tactic:
·

Goal state after:
case refine_1
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : s ∈ cobounded ℝ
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 = ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 < ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 = ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 < ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
x✝ : R
m : ℕ
x : R
n : ℕ
hx : 0 < ‖x‖
⊢ ‖↑n‖ * ‖x‖ ≤ ‖x‖
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k

pp: R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • max 1 (‖x‖ ^ m)

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case refine_2
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (cobounded ℝ ×ˢ ⊤) atTop

Tactic:
·

Goal state after:
case refine_2
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (cobounded ℝ ×ˢ ⊤) atTop
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case h
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1

pp: case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

pp: case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m

Tactic:
·

Goal state after:
case h
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case h.inl
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : max 1 (‖x‖ ^ 0) = 1
hx : ‖x‖ ^ 0 ≤ 1
hi : i ∈ Finset.range (0 + 1)
⊢ ‖x‖ ^ i ≤ 1

pp: case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
·

Goal state after:
case h.inl
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : max 1 (‖x‖ ^ 0) = 1
hx : ‖x‖ ^ 0 ≤ 1
hi : i ∈ Finset.range (0 + 1)
⊢ ‖x‖ ^ i ≤ 1
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
·

Goal state after:
case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

pp: case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m

Tactic:
·

Goal state after:
case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inl
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 = ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

pp: case inr
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 < ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

Tactic:
·

Goal state after:
case inl
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 = ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m

Tactic:
·

Goal state after:
case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : x = (algebraMap ℝ F) u
x✝ : ℝ × ℝ
⊢ x✝ ∈ univ → x✝ ∈ {x_1 | (fun x_2 ↦ (fun x_3 ↦ ‖φ x x_3‖) (u, 0) ≤ (fun x_3 ↦ ‖φ x x_3‖) x_2) x_1}

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

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

pp: case neg
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 x

Tactic:
·

Goal state after:
case pos.refine_1
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 x
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 y

Tactic:
·

Goal state after:
case pos.refine_2
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 y
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
⊢ p 1 = 1

pp: case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 = 1

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
⊢ p 1 = 1
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 = 1

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 = 1
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ f (a ^ (n + 2)) ≤ f a ^ (n + 2)

Tactic:
simp only [pow_succ _ (n + 1)]
    grw [map_mul_le_mul, map_pow_le_pow _ _ n.succ_ne_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: case zero
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
hn : 1 ≤ 0
⊢ f (x ^ 0) = f x ^ 0

pp: case succ
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n✝ : ℕ
hn : 1 ≤ n✝ + 1
⊢ f (x ^ (n✝ + 1)) = f x ^ (n✝ + 1)

Tactic:
·

Goal state after:
case zero
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
hn : 1 ≤ 0
⊢ f (x ^ 0) = f x ^ 0
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: case succ
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n✝ : ℕ
hn : 1 ≤ n✝ + 1
⊢ f (x ^ (n✝ + 1)) = f x ^ (n✝ + 1)

Tactic:
·

Goal state after:
case succ
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n✝ : ℕ
hn : 1 ≤ n✝ + 1
⊢ f (x ^ (n✝ + 1)) = f x ^ (n✝ + 1)
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
y : R
⊢ AddGroupSeminorm.toFun 1 (0 * y) = AddGroupSeminorm.toFun 1 0 * AddGroupSeminorm.toFun 1 y

pp: case inr
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x y : R
hx : x ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
y : R
⊢ AddGroupSeminorm.toFun 1 (0 * y) = AddGroupSeminorm.toFun 1 0 * AddGroupSeminorm.toFun 1 y
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
hx : x ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * 0) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 0

pp: case inr.inr
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
hx : x ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * 0) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 0
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0 x
⊢ 0 ≤ c * f x

pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : 0 x < f x
⊢ 0 ≤ c * f x

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0 x
⊢ 0 ≤ c * f x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : 0 x < f x
⊢ 0 ≤ c * f x

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : 0 x < f x
⊢ 0 ≤ c * f x
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this : (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree ≤ (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ False

pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  ((↑f.natDegree + 1) * ε) ^ ((↑f.natDegree)⁻¹ * ↑f.natDegree) * max ‖a‖ 1 ^ ↑f.natDegree ≤
    (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ ↑f.natDegree ≠ 0

Tactic:
·

Goal state after:
K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this : (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree ≤ (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ False
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : f 1 = 0
⊢ 0 ≤ c

pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : f 1 = 0
⊢ 0 ≤ c
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  ((↑f.natDegree + 1) * ε) ^ ((↑f.natDegree)⁻¹ * ↑f.natDegree) * max ‖a‖ 1 ^ ↑f.natDegree ≤
    (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ ↑f.natDegree ≠ 0

Tactic:
·

Goal state after:
K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  ((↑f.natDegree + 1) * ε) ^ ((↑f.natDegree)⁻¹ * ↑f.natDegree) * max ‖a‖ 1 ^ ↑f.natDegree ≤
    (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ ↑f.natDegree ≠ 0
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case h.inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : f y = 0 y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x

pp: case h.inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : 0 y < f y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x

Tactic:
·

Goal state after:
case h.inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : f y = 0 y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case h.inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : 0 y < f y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x

Tactic:
·

Goal state after:
case h.inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : 0 y < f y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : f y = 0 y
⊢ f (x * y) / f y ≤ c * f x

pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : 0 y < f y
⊢ f (x * y) / f y ≤ c * f x

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : f y = 0 y
⊢ f (x * y) / f y ≤ c * f x