awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
⊢ LE.le (α := ℝ) 0 (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal))

Tactic:
prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Multiset.prod_map_nonneg, Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
⊢ LE.le (α := ℝ) 0 (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal))

Tactic:
exact prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Multiset.prod_map_nonneg, Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
inr :
  LE.le (α := ℝ)
    (prod
      (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
    (prod
      (map
        (fun (i : AbsoluteValue K ℝ) ↦
          (↑(Nat.card ι) : ℝ) *
            HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι' × ι), (i : (a : K) → ℝ) (A i_1)))
        archAbsVal))
⊢ prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)

Tactic:
rw [mul_assoc, ← prod_map_mul, ← prod_replicate, totalWeight, ← map_const', ← prod_map_mul]

Premises used: Multiset.prod_replicate, mul_assoc, Multiset.prod_map_mul, Height.totalWeight, Multiset.map_const'
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
⊢ LE.le (α := ℝ)
    (prod
      (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
    (prod
      (map
        (fun (i : AbsoluteValue K ℝ) ↦
          (↑(Nat.card ι) : ℝ) *
            HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι' × ι), (i : (a : K) → ℝ) (A i_1)))
        archAbsVal))

Tactic:
prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _) fun v _ ↦ ?_

Premises used: HMul.hMul, Finset.univ, Prod.mk, Multiset.prod_map_le_prod_map₀, Real.iSup_nonneg_of_nonnegHomClass, Finset.sum
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
inr :
  ∀ (v : AbsoluteValue K ℝ),
    Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v →
      ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
        (↑(Nat.card ι) : ℝ) *
          HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) (⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i))
⊢ LE.le (α := ℝ)
    (prod
      (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
    (prod
      (map
        (fun (i : AbsoluteValue K ℝ) ↦
          (↑(Nat.card ι) : ℝ) *
            HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι' × ι), (i : (a : K) → ℝ) (A i_1)))
        archAbsVal))

Tactic:
refine prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _) fun v _ ↦ ?_

Premises used: Multiset.prod_map_le_prod_map₀, Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
v : AbsoluteValue K ℝ
h_1 : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
inr :
  ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
⊢ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
    (↑(Nat.card ι) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) (⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i))

Tactic:
rw [mul_comm (iSup _), ← mul_assoc]

Premises used: iSup, mul_assoc, mul_comm
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
v : AbsoluteValue K ℝ
h_1 : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
⊢ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)

Tactic:
v.iSup_abv_linearMap_apply_le A x

Premises used: AbsoluteValue.iSup_abv_linearMap_apply_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
v : AbsoluteValue K ℝ
h_1 : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
⊢ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)

Tactic:
exact v.iSup_abv_linearMap_apply_le A x

Premises used: AbsoluteValue.iSup_abv_linearMap_apply_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
funProp : ∀ (i : ι' × ι), A i ≠ 0
funProp₁ : A ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι' × ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
funProp : ∀ (i : ι), x i ≠ 0
funProp₁ : x ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
inr :
  LE.le (α := ℝ)
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))
    (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)),
      HMul.hMul (α := ℝ) (⨆ (i_1 : ι' × ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i_1))
        (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)))
⊢ ∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
    HMul.hMul (α := ℝ)
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι' × ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))

Tactic:
rw [← finprod_mul_distrib (by fun_prop) (by fun_prop)]

Premises used: finprod_mul_distrib
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
funProp : ∀ (i : ι'), Ne.{u_1 + 1} (α := K) (∑ i_1 : ι, A (i, i_1) * x i_1) 0
funProp₁ : Ne (α := ι' → K) (fun (i : ι') ↦ ∑ i_1 : ι, A (i, i_1) * x i_1) 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
funProp : ∀ (i : ι' × ι), A i ≠ 0
funProp₁ : A ≠ 0
funProp₂ : ∀ (i : ι), x i ≠ 0
funProp₃ : x ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (i : (↑nonarchAbsVal : Type u_1)) ↦
    HMul.hMul (α := ℝ) (⨆ (i_1 : ι' × ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i_1))
      (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
inr :
  ∀ (v : (↑nonarchAbsVal : Type u_1)),
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
      HMul.hMul (α := ℝ) (⨆ (i : ι' × ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i))
        (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ)
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))
    (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)),
      HMul.hMul (α := ℝ) (⨆ (i_1 : ι' × ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i_1))
        (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)))

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

Premises used: finprod_le_finprod
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
v : (↑nonarchAbsVal : Type u_1)
⊢ ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
    HMul.hMul (α := ℝ) (⨆ (i : ι' × ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i))
      (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))

Tactic:
(isNonarchimedean _ v.prop).iSup_abv_linearMap_apply_le A x

Premises used: Height.AdmissibleAbsValues.isNonarchimedean, IsNonarchimedean.iSup_abv_linearMap_apply_le, Subtype.prop
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
hA : A ≠ 0
hx : x ≠ 0
v : (↑nonarchAbsVal : Type u_1)
⊢ ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1) ≤
    HMul.hMul (α := ℝ) (⨆ (i : ι' × ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i))
      (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))

Tactic:
exact (isNonarchimedean _ v.prop).iSup_abv_linearMap_apply_le A x

Premises used: Height.AdmissibleAbsValues.isNonarchimedean, IsNonarchimedean.iSup_abv_linearMap_apply_le, Subtype.prop
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
inl :
  ∀ (hι : IsEmpty ι),
    (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x
inr :
  ∀ (hι : Nonempty ι),
    (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x
⊢ (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
this : 0 ≤ logHeight A + logHeight x
⊢ (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
inl : 0 ≤ logHeight A + logHeight x
⊢ (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x

Tactic:
suffices 0 ≤ logHeight A + logHeight x by simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
⊢ 0 ≤ logHeight A + logHeight x

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
⊢ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
⊢ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) ≠ 0

Tactic:
have : (Nat.card ι : ℝ) ^ totalWeight K ≠ 0 := by simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
this : HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) ≠ 0
inr :
  log (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    log (HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x)
⊢ log (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + log (mulHeight A) + log (mulHeight x)

Tactic:
pull (disch := first | assumption | positivity) log

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
this : HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) ≠ 0
⊢ 0 < mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_1
inst : Field K
ι : Type u_2
ι' : Type u_3
inst_1 : Fintype ι
inst_2 : Finite ι'
inst_3 : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
this : HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) ≠ 0
⊢ log (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    log (HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x)

Tactic:
exact (log_le_log <| by positivity) <| mulHeight_linearMap_apply_le ..

Premises used: Real.log_le_log, Height.mulHeight_linearMap_apply_le
-- 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
rw :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    (∑ i ∈ p.support,
        HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff i p) : ℝ)
          (HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N) :
      ℝ)
⊢ (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
    (Finsupp.sum p fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N

Tactic:
rw [eval_eq, sum_def, Finset.sum_mul]

Premises used: MvPolynomial.sum_def, MvPolynomial.eval_eq, Finset.sum_mul
-- 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
grw :
  LE.le (α := ℝ)
    (∑ i ∈ p.support,
      (v : (a : K) → ℝ) (coeff i p * ∏ i_1 ∈ i.support, HPow.hPow (β := ℕ) (x i_1) ((i : (a : ι) → ℕ) i_1 : ℕ)))
    (∑ i ∈ p.support,
      HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff i p) : ℝ)
        (HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N))
⊢ LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    (∑ i ∈ p.support,
        HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff i p) : ℝ)
          (HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N) :
      ℝ)

Tactic:
grw [AbsoluteValue.sum_le]

Premises used: AbsoluteValue.sum_le
-- 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
simp_rw :
  LE.le (α := ℝ)
    (∑ x_1 ∈ p.support,
      HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff x_1 p) : ℝ)
        (∏ x_2 ∈ x_1.support,
            HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_2) : ℝ) ((x_1 : (a : ι) → ℕ) x_2 : ℕ) :
          ℝ))
    (∑ i ∈ p.support,
      HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff i p) : ℝ)
        (HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N))
⊢ LE.le (α := ℝ)
    (∑ i ∈ p.support,
      (v : (a : K) → ℝ) (coeff i p * ∏ i_1 ∈ i.support, HPow.hPow (β := ℕ) (x i_1) ((i : (a : ι) → ℕ) i_1 : ℕ)))
    (∑ i ∈ p.support,
      HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff i 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 ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ LE.le (α := ℝ)
    (∑ x_1 ∈ p.support,
      HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff x_1 p) : ℝ)
        (∏ x_2 ∈ x_1.support,
            HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_2) : ℝ) ((x_1 : (a : ι) → ℕ) x_2 : ℕ) :
          ℝ))
    (∑ i ∈ p.support,
      HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff i p) : ℝ)
        (HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N))

Tactic:
Finset.sum_le_sum fun s hs ↦ ?_

Premises used: Finset.sum_le_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
refine :
  ∀ (s : ι →₀ ℕ) (hs : s ∈ p.support),
    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)
⊢ LE.le (α := ℝ)
    (∑ x_1 ∈ p.support,
      HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff x_1 p) : ℝ)
        (∏ x_2 ∈ x_1.support,
            HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_2) : ℝ) ((x_1 : (a : ι) → ℕ) x_2 : ℕ) :
          ℝ))
    (∑ i ∈ p.support,
      HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (coeff i p) : ℝ)
        (HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N))

Tactic:
refine Finset.sum_le_sum fun s hs ↦ ?_

Premises used: Finset.sum_le_sum