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
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
j : ι'
inr :
  (Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N ≤
    (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (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

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

Premises used: AbsoluteValue.eval_mvPolynomial_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
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
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
j : ι'
inr : 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
inr₁ :
  LE.le (α := ℝ) (Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
    (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
⊢ (Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N ≤
    (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c) *
      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
ι' : 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
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
j : ι'
⊢ 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
HH₁ 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))
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
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
j : ι'
⊢ 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
exact HH₁ 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))
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
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
j : ι'
⊢ LE.le (α := ℝ) (Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
    (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)

Tactic:
HH₂ (fun j ↦ Finsupp.sum (p j) fun _ c ↦ v c) j

Premises used: Finsupp.sum, 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
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
j : ι'
⊢ LE.le (α := ℝ) (Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
    (⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)

Tactic:
exact HH₂ (fun j ↦ Finsupp.sum (p j) fun _ c ↦ v c) j

Premises used: Finsupp.sum, 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
⊢ 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 ι'
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 ι'
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)

Tactic:
have F := hasFiniteMulSupport_iSup_nonarchAbsVal hx
-- 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)
⊢ 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 ι'
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)
funProp : x ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (i : (↑nonarchAbsVal : Type u_4)) ↦
    HPow.hPow (α := ℝ) (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) N

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 ι'
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 :
  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)
⊢ ∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (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) *
      HPow.hPow (α := ℝ)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N

Tactic:
rw [finprod_pow F, ← finprod_mul_distrib (by fun_prop) (by fun_prop)]

Premises used: finprod_mul_distrib, finprod_pow
-- 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)
funProp : Ne (α := ι' → K) (fun (i : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p i)) 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (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 ι'
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)
funProp : x ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (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:
fun_prop