Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case c0
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1)

pp: case b0
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤
    ↑(Nat.card ι) ^ totalWeight K * (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod *
      (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod

pp: case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod ≤
    ↑(Nat.card ι) ^ totalWeight K * (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod *
      (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod

pp: case h₂
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

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

Goal state after:
case b0
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤
    ↑(Nat.card ι) ^ totalWeight K * (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod *
      (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod

case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod ≤
    ↑(Nat.card ι) ^ totalWeight K * (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod *
      (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod

case h₂
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)