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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
inr :
  ∀ (i : ι),
    HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ ⨆ (i : ι), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
refine ciSup_le fun i ↦ ?_

Premises used: ciSup_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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
inr : LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))
inr₁ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)
inr₂ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
gcongr
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
⊢ LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))

Tactic:
Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
⊢ LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))

Tactic:
exact Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)

Tactic:
Finite.le_ciSup_of_le (j, i) le_rfl

Premises used: le_rfl, Prod.mk, Finite.le_ciSup_of_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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le (j, i) le_rfl

Premises used: le_rfl, Prod.mk, Finite.le_ciSup_of_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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_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
⊢ 1 = HMul.hMul (α := ℝ) 1 1 * 1

Tactic:
ring
-- 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
rw : HMul.hMul (α := ℝ) 1 1 * 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
⊢ 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
rw [show (1 : ℝ) = 1 * 1 * 1 by ring]
-- 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)
h₂ : 1 ≤ mulHeight A
h₃ : 1 ≤ mulHeight x
⊢ HMul.hMul (α := ℝ) 1 1 * 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
gcongr
-- 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
⊢ 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K)

Tactic:
exact_mod_cast Nat.one_le_pow _ _ Nat.card_pos

Premises used: Nat.card_pos, Nat.one_le_pow
-- 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
⊢ 1 ≤ mulHeight A

Tactic:
one_le_mulHeight _

Premises used: Height.one_le_mulHeight
-- 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
⊢ 1 ≤ mulHeight A

Tactic:
exact one_le_mulHeight _

Premises used: Height.one_le_mulHeight
-- 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
⊢ 1 ≤ mulHeight x

Tactic:
one_le_mulHeight _

Premises used: Height.one_le_mulHeight
-- 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
⊢ 1 ≤ mulHeight x

Tactic:
exact one_le_mulHeight _

Premises used: Height.one_le_mulHeight
-- 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
⊢ 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
have H₀ : 1 ≤ Nat.card ι ^ totalWeight K * mulHeight A * mulHeight x := by
    rw [show (1 : ℝ) = 1 * 1 * 1 by ring]
    gcongr
    · exact_mod_cast Nat.one_le_pow _ _ Nat.card_pos
    · exact one_le_mulHeight _
    · exact one_le_mulHeight _
-- 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
inl :
  ∀ (hι' : IsEmpty ι'),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
inr :
  ∀ (hι' : Nonempty ι'),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight 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
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : IsEmpty ι'
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
simpa only [mulHeight_eq_one_of_subsingleton, mul_one] using H₀

Premises used: Height.mulHeight_eq_one_of_subsingleton, mul_one
-- 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 ι'
inr :
  ∀ (h : Eq (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
inr₁ :
  ∀ (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
rcases eq_or_ne (fun j ↦ ∑ i, A (j, i) * x i) 0 with h | h

Premises used: HMul.hMul, Finset.univ, Prod.mk, eq_or_ne, OfNat.ofNat, 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 : Eq (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
simpa only [h, mulHeight_zero] using H₀

Premises used: Height.mulHeight_zero
-- 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
inr :
  ∀ (H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x)
    (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x
inr₁ :
  ∀ (hA : A ≠ 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
rcases eq_or_ne A 0 with rfl | hA

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 ι
x : ι → K
hι' : Nonempty ι'
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) 0
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x

Tactic:
simpa using H₀
-- 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
inr :
  ∀
    (H₀ :
      1 ≤
        HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0)
    (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
inr₁ :
  ∀ (hx : x ≠ 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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
hι' : Nonempty ι'
hA : A ≠ 0
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) 0
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0

Tactic:
simpa using H₀
-- 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 :
  HMul.hMul (α := ℝ)
      (prod
        (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) ≤
    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) *
      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))
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x

Tactic:
rw [mulHeight_eq h, mulHeight_eq hA, mulHeight_eq hx, mul_mul_mul_comm, ← mul_assoc, ← mul_assoc,
    mul_assoc (_ * _ * _)]

Premises used: HMul.hMul, mul_mul_mul_comm, mul_assoc, Height.mulHeight_eq
-- 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 (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))
inr₁ :
  0 ≤
    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)
inr₂ :
  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)
inr₃ :
  ∏ᶠ (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))
⊢ HMul.hMul (α := ℝ)
      (prod
        (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) ≤
    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) *
      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:
gcongr
-- 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
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))

Tactic:
finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _

Premises used: finprod_nonneg, HMul.hMul, Finset.univ, Prod.mk, Real.iSup_nonneg_of_nonnegHomClass, Subtype.val, 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
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))

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

Premises used: finprod_nonneg
-- 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
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K)

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
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 (α := ℝ) 0 (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
inr₁ : LE.le (α := ℝ) 0 (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal))
⊢ 0 ≤
    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:
refine mul_nonneg (mul_nonneg (by simp) ?_) ?_

Premises used: mul_nonneg
-- 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) → ℝ) (x 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) → ℝ) (x 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