mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inl
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q = 0
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

pp: case inr
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
·

Goal state after:
case inl
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q = 0
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) f)
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)

pp: case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)

Tactic:
·

Goal state after:
case inl
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) f)
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
this :
  ∀ {c : ℝ} {R : Type u_3} [inst : Ring R] {v : AbsoluteValue R ℝ},
    IsNonarchimedean ⇑v →
      0 < c →
        ∀ (p q : R[X]),
          0 ≤ c →
            ∀ (i : ℕ),
              gaussNorm v c p = v (p.coeff i) * c ^ i →
                (∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p) →
                  ∀ (j : ℕ),
                    gaussNorm v c q = v (q.coeff j) * c ^ j →
                      (∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q) →
                        v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0 →
                          gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
hvpq : ¬(v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
·

Goal state after:
case inr
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
this :
  ∀ {c : ℝ} {R : Type u_3} [inst : Ring R] {v : AbsoluteValue R ℝ},
    IsNonarchimedean ⇑v →
      0 < c →
        ∀ (p q : R[X]),
          0 ≤ c →
            ∀ (i : ℕ),
              gaussNorm v c p = v (p.coeff i) * c ^ i →
                (∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p) →
                  ∀ (j : ℕ),
                    gaussNorm v c q = v (q.coeff j) * c ^ j →
                      (∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q) →
                        v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0 →
                          gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
hvpq : ¬(v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)

Tactic:
·

Goal state after:
case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) =
    v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j)

pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ ∀ j_1 ∈ range (i + j).succ,
    j_1 ≠ i →
      v (p.coeff (j_1, i + j - j_1).1 * q.coeff (j_1, i + j - j_1).2) <
        v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2)

Tactic:
·

Goal state after:
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) =
    v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
⊢ ∀ (i : σ →₀ ℕ), (v ((coeff i) (f + g)) * i.prod fun x1 x2 ↦ c x1 ^ x2) ≤ max (gaussNorm v c f) (gaussNorm v c g)

pp: case refine_2
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
⊢ 0 ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
⊢ ∀ (i : σ →₀ ℕ), (v ((coeff i) (f + g)) * i.prod fun x1 x2 ↦ c x1 ^ x2) ≤ max (gaussNorm v c f) (gaussNorm v c g)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case e'_3
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) * c ^ (i + j) =
    v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x))

pp: case e'_4
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j) =
    v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

Tactic:
·

Goal state after:
case e'_3
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) * c ^ (i + j) =
    v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x))
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : P.degree ≤ 0
⊢ 0 < eval x P

pp: case neg
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
⊢ 0 < eval x P

Tactic:
·

Goal state after:
case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
hdeg : P.degree ≤ 0
⊢ 0 < eval x P
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ y, P.IsRoot y ∧ x ≤ y
⊢ 0 ≤ eval x P

pp: case neg
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), P.IsRoot y → y < x
⊢ 0 ≤ eval x P

Tactic:
·

Goal state after:
case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ y, P.IsRoot y ∧ x ≤ y
⊢ 0 ≤ eval x P
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
h :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c f ∨
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c g

pp: case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
h :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c f ∨
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c g

Tactic:
·

Goal state after:
case inl
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
h :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c f ∨
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c g
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case neg
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), P.IsRoot y → y < x
⊢ 0 ≤ eval x P

Tactic:
·

Goal state after:
case neg
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), P.IsRoot y → y < x
⊢ 0 ≤ eval x P
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
h :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c f ∨
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c g

Tactic:
·

Goal state after:
case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
h :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c f ∨
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤ gaussNorm v c g
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y

pp: case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
·

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case e'_4
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j) =
    v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

Tactic:
·

Goal state after:
case e'_4
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j) =
    v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
·

Goal state after:
case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y

pp: case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
·

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
·

Goal state after:
case refine_2
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff