awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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
⊢ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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
⊢ (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

Premises used: eq_or_ne, MvPolynomial.constantCoeff, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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:
simp [h]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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:
simpa using le_max_of_le_left <| mulHeight_constantCoeff_le_mulHeightBound h

Premises used: le_max_of_le_left, _private.0.Height.mulHeight_constantCoeff_le_mulHeightBound
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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
⊢ (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₀

Premises used: MvPolynomial.eval, eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
inr : (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤ 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

Tactic:
grw [← le_max_right]

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)) ≤ 1 * mulHeight x ^ N

Tactic:
simpa [h₀, mulHeight_zero] using one_le_pow₀ <| one_le_mulHeight x

Premises used: Height.one_le_mulHeight, one_le_pow₀, Height.mulHeight_zero
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
v : AbsoluteValue K ℝ
j : ι'
s : ι →₀ ℕ
⊢ LE.le (α := ℝ) (0 : ℝ) ((v : (a : K) → ℝ) ((p j : (a : ι →₀ ℕ) → K) s : K) : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ ∀ (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)
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
⊢ 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
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))
⊢ 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 ..
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))
⊢ 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 ..
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))
⊢ 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 ..
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ (j : ι'), f j

Tactic:
have HH₂ (f : ι' → ℝ) (j : ι') : f j ≤ ⨆ j, f j := Finite.le_ciSup ..
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ (j : ι'), f j
inr :
  HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦
            ⨆ (i : ι'), (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K)) ≤
    max
        (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))
        1 *
      HMul.hMul (α := ℝ)
          (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
          (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (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

Tactic:
simp only [mulHeight_eq hx, mulHeight_eq h₀, mulHeightBound_eq]

Premises used: Height.mulHeight_eq, Height.mulHeightBound_eq
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ (j : ι'), f j
inr :
  LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
        archAbsVal))
    (Multiset.prod
      (Multiset.map
        (fun (i : AbsoluteValue K ℝ) ↦
          (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (i : (a : K) → ℝ) c) *
            HPow.hPow (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) N)
        archAbsVal))
⊢ Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) ((eval x : (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) *
      HPow.hPow (α := ℝ)
        (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal)) N

Tactic:
rw [← prod_map_pow, ← prod_map_mul]

Premises used: Multiset.prod_map_pow, Multiset.prod_map_mul
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ (j : ι'), f j
⊢ LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
        archAbsVal))
    (Multiset.prod
      (Multiset.map
        (fun (i : AbsoluteValue K ℝ) ↦
          (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (i : (a : K) → ℝ) c) *
            HPow.hPow (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) N)
        archAbsVal))

Tactic:
prod_map_le_prod_map₀ _ _ (fun _ _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..)
      fun v _ ↦ Real.iSup_le (fun j ↦ ?_) <| mul_nonneg (H₀ v) (HH₁ v)

Premises used: mul_nonneg, MvPolynomial.eval, Multiset.prod_map_le_prod_map₀, Real.iSup_le, Real.iSup_nonneg_of_nonnegHomClass, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ (j : ι'), f j
inr :
  ∀ (v : AbsoluteValue K ℝ),
    Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v →
      ∀ (j : ι'),
        (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) ≤
          (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c) *
            HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
        archAbsVal))
    (Multiset.prod
      (Multiset.map
        (fun (i : AbsoluteValue K ℝ) ↦
          (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (i : (a : K) → ℝ) c) *
            HPow.hPow (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) N)
        archAbsVal))

Tactic:
refine prod_map_le_prod_map₀ _ _ (fun _ _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..)
      fun v _ ↦ Real.iSup_le (fun j ↦ ?_) <| mul_nonneg (H₀ v) (HH₁ v)

Premises used: mul_nonneg, Multiset.prod_map_le_prod_map₀, Real.iSup_le, Real.iSup_nonneg_of_nonnegHomClass