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
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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
inr :
  ∀ (v : (↑nonarchAbsVal : Type u_4)) (j : ι'),
    ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) ≤
      (⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
        HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
inr₁ :
  ∀ (v : (↑nonarchAbsVal : Type u_4)),
    0 ≤
      (⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
        HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
⊢ LE.le (α := ℝ)
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p i) : K))
    (∏ᶠ (i : (↑nonarchAbsVal : Type u_4)),
      (⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
        HPow.hPow (α := ℝ) (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) N)

Tactic:
refine finprod_le_finprod (by fun_prop)
      (fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) fun v ↦ Real.iSup_le
      (fun j ↦ ?_) ?_

Premises used: finprod_le_finprod, Real.iSup_le, 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))
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ (j : ι'), f j
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
inr :
  (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
⊢ ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N

Tactic:
grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x]

Premises used: Height.AdmissibleAbsValues.isNonarchimedean, IsNonarchimedean.eval_mvPolynomial_le, Subtype.prop
-- 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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
inr : 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
inr₁ :
  LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
⊢ (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N

Tactic:
gcongr
-- 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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
⊢ 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N

Tactic:
HH₁ v.val

Premises used: Subtype.val
-- 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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
⊢ 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N

Tactic:
exact HH₁ v.val

Premises used: Subtype.val
-- 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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
inr :
  LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
inr₁ : ι'
inr₂ :
  LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
inr₃ : ι'
inr₄ :
  LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
inr₅ : ι'
⊢ LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)

Tactic:
grw [← HH₂, ← le_max_left]

Premises used: le_max_left
-- 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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
x_1 : ι'
⊢ LE.le (α := ℝ) 0
    (max (⨆ (s : ↥(p x_1).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p x_1))) 1)

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
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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
⊢ 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N

Tactic:
simp only [HH₁]
-- 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
this : Nonempty ι'
F :
  Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
v : (↑nonarchAbsVal : Type u_4)
⊢ 0 ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N

Tactic:
exact mul_nonneg (iSup_nonneg fun _ ↦ by positivity) <| by simp only [HH₁]

Premises used: mul_nonneg, Real.iSup_nonneg
-- 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
⊢ max (mulHeightBound p) 1 > 0

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
pull :
  log (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    log (max (mulHeightBound p) 1 * mulHeight x ^ N)
⊢ log (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    log (max (mulHeightBound p) 1) + (↑N : ℝ) * log (mulHeight x)

Tactic:
pull (disch := positivity) log

Premises used: Real.log
-- 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
⊢ 0 < mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)

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
⊢ log (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    log (max (mulHeightBound p) 1 * mulHeight x ^ N)

Tactic:
exact (log_le_log <| by positivity) <| mulHeight_eval_le hp x

Premises used: Real.log_le_log, Height.mulHeight_eval_le
-- 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
⊢ ∃ (C : ℝ),
    ∀ (x : ι → K),
      (logHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
        C + (↑N : ℝ) * logHeight x

Tactic:
⟨_, logHeight_eval_le hp⟩

Premises used: Height.logHeight_eval_le, Exists.intro
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
M N : ℕ
q : ι × ι' → MvPolynomial ι K
inst_2 : IsEmpty ι'
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h₁ : ∀ (i : ι), x i = 0 i
⊢ x = 0

Tactic:
ext i
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
M N : ℕ
q : ι × ι' → MvPolynomial ι K
inst_2 : IsEmpty ι'
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
i : ι
⊢ ∀ (k : ι), 0 = x k ^ (M + N)

Tactic:
simp only [Finset.univ_eq_empty, Finset.sum_empty] at h

Premises used: Finset.univ_eq_empty, Finset.sum_empty
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
M N : ℕ
q : ι × ι' → MvPolynomial ι K
inst_2 : IsEmpty ι'
p : ι' → MvPolynomial ι K
x : ι → K
i : ι
h : ∀ (k : ι), 0 = x k ^ (M + N)
⊢ x i = 0 i

Tactic:
eq_zero_of_pow_eq_zero <| (h i).symm

Premises used: eq_zero_of_pow_eq_zero, Eq.symm
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
M N : ℕ
q : ι × ι' → MvPolynomial ι K
inst_2 : IsEmpty ι'
p : ι' → MvPolynomial ι K
x : ι → K
i : ι
h : ∀ (k : ι), 0 = x k ^ (M + N)
⊢ x i = 0 i

Tactic:
exact eq_zero_of_pow_eq_zero <| (h i).symm

Premises used: eq_zero_of_pow_eq_zero, Eq.symm
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
inl :
  IsEmpty ι' →
    (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
inr :
  Nonempty ι' →
    (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)

Tactic:
rcases isEmpty_or_nonempty ι'

Premises used: isEmpty_or_nonempty