awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
c0 :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
b0 :
  LE.le (α := ℝ) 0
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
h₁ :
  LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦
          ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
        archAbsVal))
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦
            ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K)) ≤
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have h₂ : LE.le (α := ℝ)
  (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
  (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
    ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦
          ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
        archAbsVal))
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
have H : ∀ (v : AbsoluteValue K ℝ) (j : ι'),
  LE.le (α := ℝ) ((v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p j) : K) : ℝ)
    (Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c : ℝ)
Tactic: have H (v : AbsoluteValue K ℝ) (j : ι') : v (constantCoeff (p j)) ≤ sum (p j) fun _ c ↦ v c :=
      single_eval_le_sum _ v.map_zero (fun _ ↦ by positivity) _
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ LE.le (α := ℝ)
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have this : Nonempty ι'
Tactic: have := (Function.ne_iff.mp h).nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
⊢ LE.le (α := ℝ)
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have h₂ : LE.le.{u_4} (α := (↑nonarchAbsVal : Type u_4) → ℝ)
  (fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
  fun (v : (↑nonarchAbsVal : Type u_4)) ↦
  ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
Tactic: refine finprod_le_finprod (by fun_prop)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
⊢ LE.le.{u_4} (α := (↑nonarchAbsVal : Type u_4) → ℝ)
    (fun (v : (↑nonarchAbsVal : Type u_4)) ↦
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
    fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
have h₂ : ∀ (v : (↑nonarchAbsVal : Type u_4)) (j : ι'),
  LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
    (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p j) : K) : ℝ)
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
Tactic: refine fun v ↦ Finite.ciSup_mono fun j ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
v : (↑nonarchAbsVal : Type u_4)
j : ι'
⊢ LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
    (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p j) : K) : ℝ)
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
have h₂ : LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
  (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff 0 (p j)) : ℝ)
  (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
Tactic: rw [show constantCoeff (p j) = coeff 0 (p j) from rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
v : (↑nonarchAbsVal : Type u_4)
j : ι'
⊢ LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
    (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff 0 (p j)) : ℝ)
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
have h₂ : ∀ (h₀ : coeff 0 (p j) = 0),
  LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
    (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff 0 (p j)) : ℝ)
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
Tactic: rcases eq_or_ne (coeff 0 (p j)) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
v : (↑nonarchAbsVal : Type u_4)
j : ι'
h₂ :
  ∀ (h₀ : coeff 0 (p j) = 0),
    LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
      (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff 0 (p j)) : ℝ)
      (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
⊢ LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
    (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff 0 (p j)) : ℝ)
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
have h₃ : ∀ (h₀ : coeff 0 (p j) ≠ 0),
  LE.le (α := (fun (a : (↑nonarchAbsVal : Type u_4)) ↦ ℝ) v)
    (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff 0 (p j)) : ℝ)
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1 : ℝ)
Tactic: rcases eq_or_ne (coeff 0 (p j)) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have inl : (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval 0 : (a : MvPolynomial ι K) → K) (p j)) ≤
  max (mulHeightBound p) 1 * mulHeight.{u_4, u_5} (K := K) (ι := ι) 0 ^ N
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
inl :
  (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval 0 : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight.{u_4, u_5} (K := K) (ι := ι) 0 ^ N
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have inr : ∀ (hx : x ≠ 0),
  (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval 0 : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight.{u_4, u_5} (K := K) (ι := ι) 0 ^ N
have inl : ∀ (h : Eq (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0),
  (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval 0 : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight.{u_4, u_5} (K := K) (ι := ι) 0 ^ N
Tactic: rcases eq_or_ne (fun j ↦ constantCoeff (p j)) 0 with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
inl :
  ∀ (h : Eq (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0),
    (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval 0 : (a : MvPolynomial ι K) → K) (p j)) ≤
      max (mulHeightBound p) 1 * mulHeight.{u_4, u_5} (K := K) (ι := ι) 0 ^ N
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval 0 : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight.{u_4, u_5} (K := K) (ι := ι) 0 ^ N
have inl₁ : ∀ (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0),
  (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval 0 : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight.{u_4, u_5} (K := K) (ι := ι) 0 ^ N
Tactic: rcases eq_or_ne (fun j ↦ constantCoeff (p j)) 0 with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have inr : ∀ (h₀ : Eq (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0),
  (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
Tactic: rcases eq_or_ne (fun j ↦ eval x (p j)) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
inr :
  ∀ (h₀ : Eq (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0),
    (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
      max (mulHeightBound p) 1 * mulHeight x ^ N
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have inr₁ : ∀ (h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0),
  (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
Tactic: rcases eq_or_ne (fun j ↦ eval x (p j)) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Eq (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have inr : (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤ 1 * mulHeight x ^ N
Tactic: grw [← le_max_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have H₀ : ∀ (v : AbsoluteValue K ℝ),
  LE.le (α := ℝ) 0 (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
Tactic: have H₀ (v : AbsoluteValue K ℝ) : 0 ≤ ⨆ j, Finsupp.sum (p j) fun _ c ↦ v c :=
    iSup_nonneg (fun j ↦ sum_nonneg' <| fun s ↦ by positivity)
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
H₀ :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) 0 (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have H₁ : LE.le (α := ℝ) 0
  (Multiset.prod
    (Multiset.map
      (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
      archAbsVal))
Tactic: have H₁ : 0 ≤ (archAbsVal.map (fun v ↦ ⨆ j, Finsupp.sum (p j) fun _ c ↦ v c)).prod :=
    prod_map_nonneg fun v _ ↦ H₀ v
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
H₀ :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) 0 (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
H₁ :
  LE.le (α := ℝ) 0
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have H₂ : LE.le (α := ℝ) 0
  (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
Tactic: have H₂ : 0 ≤ (archAbsVal.map (fun v ↦ ⨆ i, v (x i))).prod :=
    prod_map_nonneg fun _ _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
H₀ :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) 0 (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
H₁ :
  LE.le (α := ℝ) 0
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
H₂ :
  LE.le (α := ℝ) 0
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have H₃ : LE.le (α := ℝ) 0
  (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
Tactic: have H₃ : 0 ≤ ∏ᶠ v : nonarchAbsVal, ⨆ i, v.val ((eval x) (p i)) :=
    finprod_nonneg fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
H₀ :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) 0 (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
H₁ :
  LE.le (α := ℝ) 0
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
H₂ :
  LE.le (α := ℝ) 0
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
H₃ :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have H₄ : LE.le (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
Tactic: have H₄ : 0 ≤ ∏ᶠ v : nonarchAbsVal, ⨆ i, v.val (x i) :=
    finprod_nonneg fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
H₀ :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) 0 (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
H₁ :
  LE.le (α := ℝ) 0
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
H₂ :
  LE.le (α := ℝ) 0
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
H₃ :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
H₄ : LE.le (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: have HH₁ (v : AbsoluteValue K ℝ) : 0 ≤ (⨆ i, v (x i)) ^ N :=
    pow_nonneg (Real.iSup_nonneg_of_nonnegHomClass v _) N
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
inst_3 : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) 0
H₀ :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) 0 (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
H₁ :
  LE.le (α := ℝ) 0
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
H₂ :
  LE.le (α := ℝ) 0
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
H₃ :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
H₄ : LE.le (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    max (mulHeightBound p) 1 * mulHeight x ^ N
have HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ (j : ι'), f j
Tactic: have HH₂ (f : ι' → ℝ) (j : ι') : f j ≤ ⨆ j, f j := Finite.le_ciSup ..