awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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) ≤
    (↑(Nat.card ι) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) (⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i))
have 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)
Tactic: rw [mul_comm (iSup _), ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι' × ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (A i)
have funProp : ∀ (i : ι' × ι), A i ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
have funProp : ∀ (i : ι), x i ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 (α := ℝ)
      (∏ᶠ (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))
have 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)))
Tactic: rw [← finprod_mul_distrib (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)
have funProp : ∀ (i : ι'), Ne.{u_1 + 1} (α := K) (∑ i_1 : ι, A (i, i_1) * x i_1) 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ 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))
have funProp : ∀ (i : ι' × ι), A i ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 (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))
have funProp₂ : ∀ (i : ι), x i ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 (α := ℝ)
    (∏ᶠ (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)))
have 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))
Tactic: refine finprod_le_finprod (by fun_prop)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _) (by fun_prop) fun v ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x
have 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
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x
have 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
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 ι
⊢ (logHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + logHeight A + logHeight x
have inl : 0 ≤ logHeight A + logHeight x
Tactic: suffices 0 ≤ logHeight A + logHeight x by simp
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
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 ι
⊢ 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)
have this : HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) ≠ 0
Tactic: have : (Nat.card ι : ℝ) ^ totalWeight K ≠ 0 := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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) ≤
    (↑(totalWeight K) : ℝ) * log (↑(Nat.card ι) : ℝ) + log (mulHeight A) + log (mulHeight x)
have 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)
Tactic: pull (disch := first | assumption | positivity) log
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ (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
have 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) :
    ℝ)
Tactic: rw [eval_eq, sum_def, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 (α := ℝ)
    ((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) :
      ℝ)
have 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))
Tactic: grw [AbsoluteValue.sum_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 (α := ℝ)
    (∑ 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))
have 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))
Tactic: simp_rw [v.map_mul, v.map_prod, v.map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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))
have 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)
Tactic: refine Finset.sum_le_sum fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
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)
have hbc : ∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) ≤
  HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ ∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) ≤
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have hbc : LE.le (α := ℝ)
  (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ))
  (∏ i ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ((s : (a : ι) → ℕ) i : ℕ))
Tactic: rw [hp.degree_eq_sum_deg_support hs, ← Finset.prod_pow_eq_pow_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ LE.le (α := ℝ)
    (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ))
    (∏ i ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ((s : (a : ι) → ℕ) i : ℕ))
have hbc : ∀ i ∈ s.support, LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have inl : ∀ (hp : IsHomogeneous.{u_5, u_4} (σ := ι) (R := K) 0 N),
  (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) 0 : K) ≤
    (⨆ (s : ↥(support.{u_4, u_5} (R := K) 0)), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) 0)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: rcases eq_or_ne p 0 with rfl | hp₀
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
inl :
  ∀ (hp : IsHomogeneous.{u_5, u_4} (σ := ι) (R := K) 0 N),
    (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) 0 : K) ≤
      (⨆ (s : ↥(support.{u_4, u_5} (R := K) 0)), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) 0)) *
        HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
⊢ (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have inr : ∀ (hp₀ : p ≠ 0),
  (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: rcases eq_or_ne p 0 with rfl | hp₀
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
⊢ (v : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) p : K) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have inr : (v : (a : K) → ℝ) (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
  (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: rw [eval_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
⊢ (v : (a : K) → ℝ) (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have inr : ∀ (s : ι →₀ ℕ) (hs₁ : s ∈ p.support)
  (hs₂ :
    LE.le (α := ℝ)
      ((v : (a : K) → ℝ)
          (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
        ℝ)
      ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)),
  (v : (a : K) → ℝ) (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: obtain ⟨s, hs₁, hs₂⟩ :=
    hv.finset_image_add_of_nonempty (fun d ↦ coeff d p * ∏ i ∈ d.support, x i ^ d i)
      (support_nonempty.mpr hp₀)
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
⊢ (v : (a : K) → ℝ) (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have inr : (v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) ≤
  (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: grw [hs₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
⊢ (v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have inr : HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ)
    (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) : ℝ) ≤
  (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
Tactic: simp_rw [v.map_mul, v.map_prod, v.map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
inst_1 : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ :
  LE.le (α := ℝ)
    ((v : (a : K) → ℝ)
        (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, HPow.hPow (β := ℕ) (x i) ((d : (a : ι) → ℕ) i : ℕ)) :
      ℝ)
    ((v : (a : K) → ℝ) (coeff s p * ∏ i ∈ s.support, HPow.hPow (β := ℕ) (x i) ((s : (a : ι) → ℕ) i : ℕ)) : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ)
      (∏ x_1 ∈ s.support, HPow.hPow (α := ℝ) (β := ℕ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ((s : (a : ι) → ℕ) x_1 : ℕ) : ℝ) ≤
    (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p)) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) N
have inr : LE.le (α := ℝ) 0 (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p))
Tactic: gcongr