awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have this : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
Tactic: have := hvpq.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have this₁ : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
Tactic: have := hvpq.2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have apply : gaussNorm v c p * gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p * q).coeff (i + j)) : ℝ) (c ^ (i + j))
Tactic: apply le_of_eq_of_le _ <| (p * q).le_gaussNorm v hc0 (i + j)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
⊢ gaussNorm v c p * gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p * q).coeff (i + j)) : ℝ) (c ^ (i + j))
have rw : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j) =
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
Tactic: rw [hi_p, hj_q, coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
    IsNonarchimedean.apply_sum_eq_of_lt hna (k := i) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
rw :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
⊢ gaussNorm v c p * gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p * q).coeff (i + j)) : ℝ) (c ^ (i + j))
have rw₁ : ∀ j_1 ∈ range (i + j).succ,
  j_1 ≠ i →
    LT.lt (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (j_1, i + j - j_1).1 * q.coeff (j_1, i + j - j_1).2) : ℝ)
      ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ)
Tactic: rw [hi_p, hj_q, coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
    IsNonarchimedean.apply_sum_eq_of_lt hna (k := i) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
⊢ LT.lt (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ)
have apply : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) <
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
Tactic: apply lt_of_mul_lt_mul_right _ <| pow_nonneg hc0 (i + j)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
have this₁ : x + (i + j - x) = i + j
Tactic: have : x + (i + j - x) = i + j := by simp_all
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
have h : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) =
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x))
Tactic: convert_to 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x))
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
have h₁ : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j)) =
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
Tactic: convert_to 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x))
h₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
have convert_to : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
Tactic: convert_to 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
have inl : x < i →
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
Tactic: rcases lt_or_gt_of_ne hneq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
inl :
  x < i →
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
        HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
        HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
have inr : i < x →
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
Tactic: rcases lt_or_gt_of_ne hneq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h : x < i
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) ≤
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) * gaussNorm v c q
have hbc : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) ≤ gaussNorm v c q
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h : x < i
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) * gaussNorm v c q =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
have rw : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j) =
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
Tactic: rw [hj_q]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h : x < i
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
have hbc : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) <
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: gcongr 1