awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
hbc :
  ∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) ≤
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ)
      (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) : ℝ) ≤
    HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ) (HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
hbc :
  LE.le (α := ℝ)
    (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ))
    (∏ i ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ((s : (a : ι) → ℕ) i : ℕ))
⊢ ∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) ≤
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
rw [hp.degree_eq_sum_deg_support hs, ← Finset.prod_pow_eq_pow_sum]

Premises used: MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support, Finset.prod_pow_eq_pow_sum
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
hbc : ∀ i ∈ s.support, LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
⊢ LE.le (α := ℝ)
    (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ))
    (∏ i ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ((s : (a : ι) → ℕ) i : ℕ))

Tactic:
gcongr with i
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
i : ι
h : i ∈ s.support
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
Finite.le_ciSup (fun j ↦ v (x j)) i

Premises used: Finite.le_ciSup, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
i : ι
h : i ∈ s.support
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
exact Finite.le_ciSup (fun j ↦ v (x j)) i

Premises used: Finite.le_ciSup, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
inl :
  ∀ (hp : IsHomogeneous.{u_5, u_4} (σ := ι) (R := K) 0 N),
    (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) 0 : K) ≤
      (⨆ (s : ↥(support.{u_4, u_5} (R := K) 0)), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) 0)) *
        HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
inr :
  ∀ (hp₀ : p ≠ 0),
    (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
      (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
        HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
rcases eq_or_ne p 0 with rfl | hp₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
N : ℕ
x : ι → K
hp : IsHomogeneous.{u_5, u_4} (σ := ι) (R := K) 0 N
⊢ (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) 0 : K) ≤
    (⨆ (s : ↥(support.{u_4, u_5} (R := K) 0)), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) 0)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
inr :
  (v : (a : K) → ℝ) (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
rw [eval_eq]

Premises used: MvPolynomial.eval_eq
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
inr :
  ∀ (s : ι →₀ ℕ) (hs₁ : s ∈ p.support)
    (hs₂ :
      LE.le (α := ℝ)
        ((v : (a : K) → ℝ)
            (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
          ℝ)
        ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)),
    (v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
      (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
        HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (v : (a : K) → ℝ) (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
obtain ⟨s, hs₁, hs₂⟩ :=
    hv.finset_image_add_of_nonempty (fun d ↦ coeff d p * ∏ i ∈ d.support, x i ^ d i)
      (support_nonempty.mpr hp₀)

Premises used: Iff.mpr, HMul.hMul, Finsupp.support, MvPolynomial.coeff, Finset.prod, IsNonarchimedean.finset_image_add_of_nonempty, MvPolynomial.support_nonempty, HPow.hPow, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
inr :
  (v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (v : (a : K) → ℝ) (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
grw [hs₂]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
inr :
  HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ)
      (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) : ℝ) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
simp_rw [v.map_mul, v.map_prod, v.map_pow]

Premises used: AbsoluteValue.map_pow, AbsoluteValue.map_prod, AbsoluteValue.map_mul
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
inr : LE.le (α := ℝ) 0 (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p))
inr₁ :
  LE.le (α := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ) (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p) : ℝ)
inr₂ :
  ∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) ≤
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ)
      (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) : ℝ) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
⊢ LE.le (α := ℝ) 0 (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p))

Tactic:
Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
⊢ LE.le (α := ℝ) 0 (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p))

Tactic:
exact Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ) (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p) : ℝ)

Tactic:
Finite.le_ciSup_of_le (⟨s, hs₁⟩ : p.support) le_rfl

Premises used: le_rfl, Subtype.mk, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ) (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le (⟨s, hs₁⟩ : p.support) le_rfl

Premises used: le_rfl, Subtype.mk, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
inr :
  LE.le (α := ℝ)
    (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ))
    (∏ i ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ((s : (a : ι) → ℕ) i : ℕ))
⊢ ∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) ≤
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
rw [hp.degree_eq_sum_deg_support hs₁, ← Finset.prod_pow_eq_pow_sum]

Premises used: MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support, Finset.prod_pow_eq_pow_sum
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
inr : ∀ i ∈ s.support, LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
⊢ LE.le (α := ℝ)
    (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ))
    (∏ i ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ((s : (a : ι) → ℕ) i : ℕ))

Tactic:
gcongr with i
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
i : ι
h : i ∈ s.support
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
Finite.le_ciSup (fun j ↦ v (x j)) i

Premises used: Finite.le_ciSup, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
i : ι
h : i ∈ s.support
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
exact Finite.le_ciSup (fun j ↦ v (x j)) i

Premises used: Finite.le_ciSup, 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
p : ι' → MvPolynomial ι K
⊢ mulHeightBound p =
    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)

Tactic:
rfl

Premises used: Height.mulHeightBound, rfl
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
simp :
  max
      (HMul.hMul (α := ℝ)
        (Multiset.prod
          (Multiset.map
            (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum 0 fun (x_1 : ι →₀ ℕ) (c : K) ↦ (x : (a : K) → ℝ) c)
            archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
⊢ max (mulHeightBound.{u_4, u_5, u_6} (K := K) (ι := ι) (ι' := ι') 0) 1 = 1

Tactic:
simp only [mulHeightBound_eq, Pi.zero_apply, support_zero, coeff_zero, AbsoluteValue.map_zero,
    Real.iSup_of_isEmpty, zero_le_one, sup_of_le_right]

Premises used: Pi.zero_apply, Real.iSup_of_isEmpty, zero_le_one, sup_of_le_right, Height.mulHeightBound_eq, MvPolynomial.coeff_zero, MvPolynomial.support_zero, AbsoluteValue.map_zero
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
simp :
  max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
⊢ max
      (HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), 0) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1

Tactic:
simp only [Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate, zero_pow_eq]

Premises used: Multiset.prod_replicate, Real.iSup_const_zero, zero_pow_eq, Multiset.map_const'
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inl :
  IsEmpty ι' →
    max
        (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
          (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
        1 =
      1
inr :
  Nonempty ι' →
    max
        (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
          (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
        1 =
      1
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1

Tactic:
rcases isEmpty_or_nonempty ι'

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
h : IsEmpty ι'
pos :
  Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 →
    max (HMul.hMul (α := ℝ) 1 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1)) 1 = 1
neg :
  ¬Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 →
    max (HMul.hMul (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1)) 1 = 1
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
h : IsEmpty ι'
h_1 : Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0
⊢ max (HMul.hMul (α := ℝ) 1 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1)) 1 = 1

Tactic:
simpa using finprod_zero_le_one

Premises used: finprod_zero_le_one
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
h : IsEmpty ι'
h_1 : ¬Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0
⊢ max (HMul.hMul (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1)) 1 = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
h : Nonempty ι'
inr : LE.le (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0) 1
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
h : Nonempty ι'
⊢ LE.le (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0) 1

Tactic:
grind