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
set_option :
  max
      (HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), 0) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
set_option₁ :
  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
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 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 (α := ℝ)
        (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

Tactic:
set_option backward.isDefEq.respectTransparency false in -- temporary measure
  simp only [Finsupp.sum_zero_index] -- singling this out for needing the above
  simp only [Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate, zero_pow_eq]
  rcases isEmpty_or_nonempty ι'
  · split_ifs
    · simpa using finprod_zero_le_one
    · simp
  · simp
    grind

Premises used: Multiset.prod_replicate, isEmpty_or_nonempty, finprod_zero_le_one, Real.iSup_const_zero, zero_pow_eq, Finsupp.sum_zero_index, 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
inst_2 : Finite ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1

Tactic:
HasFiniteMulSupport.iSup fun j ↦ ?_

Premises used: Function.HasFiniteMulSupport.iSup
-- 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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
refine :
  ∀ (j : ι'),
    HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
      max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1

Tactic:
refine HasFiniteMulSupport.iSup fun j ↦ ?_

Premises used: Function.HasFiniteMulSupport.iSup
-- 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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
inl :
  ∀ (hs₀ : IsEmpty.{u_5 + 1} ↥(p j).support),
    HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
      max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
inr :
  ∀ (hs₀ : Nonempty.{u_5 + 1} ↥(p j).support),
    HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
      max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1

Tactic:
rcases isEmpty_or_nonempty (p j).support with hs₀ | hs₀

Premises used: Membership.mem, isEmpty_or_nonempty, Subtype, MvPolynomial.support
-- 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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : IsEmpty.{u_5 + 1} ↥(p j).support
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1

Tactic:
simp [hasFiniteMulSupport_one]

Premises used: Function.hasFiniteMulSupport_one
-- 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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : Nonempty.{u_5 + 1} ↥(p j).support
⊢ ∀ (s : ↥(p j).support), coeff (↑s : ι →₀ ℕ) (p j) ≠ 0

Tactic:
have H (s : (p j).support) : coeff s.val (p j) ≠ 0 := mem_support_iff.mp s.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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : Nonempty.{u_5 + 1} ↥(p j).support
H : ∀ (s : ↥(p j).support), coeff (↑s : ι →₀ ℕ) (p j) ≠ 0
i : ↥(p j).support
⊢ coeff (↑i : ι →₀ ℕ) (p j) ≠ 0

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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : Nonempty.{u_5 + 1} ↥(p j).support
H funProp : ∀ (i : ↥(p j).support), coeff (↑i : ι →₀ ℕ) (p j) ≠ 0
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1

Tactic:
fun_prop (disch := 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
simp :
  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)
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) ≤ mulHeightBound p

Tactic:
simp only [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 ι'
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))
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)
⊢ 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)

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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))

Tactic:
finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..

Premises used: finprod_nonneg, Real.iSup_nonneg_of_nonnegHomClass, MvPolynomial.constantCoeff, Subtype.val, 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))

Tactic:
exact finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..

Premises used: finprod_nonneg, 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
v : AbsoluteValue K ℝ
h_1 : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
x : ι'
x_1 : ι →₀ ℕ
h_2 : x_1 ∈ (p x).support
⊢ LE.le (α := ℝ) (0 : ℝ) ((v : (a : K) → ℝ) ((p x : (a : ι →₀ ℕ) → K) x_1 : 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ 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:
exact prod_map_nonneg fun v _ ↦ iSup_nonneg fun _ ↦ sum_nonneg fun _ _ ↦ 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
v : AbsoluteValue K ℝ
j : ι'
x : K
⊢ LE.le (α := (fun (x : K) ↦ ℝ) x) (0 x) ((fun (x : K) ↦ ((v : (a : K) → ℝ) x : ℝ)) x)

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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ ∀ (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) _
-- 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
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 : ℝ)
⊢ 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))

Tactic:
prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..)
      fun v _ ↦ Finite.ciSup_mono (H v)

Premises used: Multiset.prod_map_le_prod_map₀, Finite.ciSup_mono, Real.iSup_nonneg_of_nonnegHomClass, MvPolynomial.constantCoeff, 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
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 : ℝ)
⊢ 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))

Tactic:
exact prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..)
      fun v _ ↦ Finite.ciSup_mono (H v)

Premises used: Multiset.prod_map_le_prod_map₀, Finite.ciSup_mono, 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ Nonempty ι'

Tactic:
have := (Function.ne_iff.mp h).nonempty
-- 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
funProp : Ne (α := ι' → K) (fun (i : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p i)) 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K)

Tactic:
fun_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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1

Tactic:
fun_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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
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
⊢ 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:
refine finprod_le_finprod (by fun_prop)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) ?_

Premises used: finprod_le_finprod, 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 ι'
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

Tactic:
fun v ↦ Finite.ciSup_mono fun j ↦ ?_

Premises used: Finite.ciSup_mono
-- 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
this : Nonempty ι'
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 : ℝ)
⊢ 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 fun v ↦ Finite.ciSup_mono fun j ↦ ?_

Premises used: Finite.ciSup_mono
-- 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 ι'
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₂ :
  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) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p j) : K) : ℝ)
    (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]

Premises used: 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 ι'
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 : ℝ)
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 : ℝ)

Tactic:
rcases eq_or_ne (coeff 0 (p j)) 0 with h₀ | h₀

Premises used: MvPolynomial.coeff, eq_or_ne, OfNat.ofNat
-- 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 ι'
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₀ : 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:
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 ι'
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₀ : coeff 0 (p j) ≠ 0
⊢ 0 ∈ (p j).support

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 ι'
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₀ : 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:
exact le_sup_of_le_left <| Finite.le_ciSup_of_le ⟨0, by simp [h₀]⟩ le_rfl

Premises used: le_rfl, le_sup_of_le_left, Finite.le_ciSup_of_le