awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 :
  ∀ (v : (↑nonarchAbsVal : Type u_4)) (j : ι'),
    ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) ≤
      (⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
        HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
⊢ 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)
have inr₁ : ∀ (v : (↑nonarchAbsVal : Type u_4)),
  0 ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
Tactic: refine finprod_le_finprod (by fun_prop)
      (fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) fun v ↦ Real.iSup_le
      (fun j ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
⊢ ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
have inr : (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) *
    HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N ≤
  (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
    HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
Tactic: grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
⊢ (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
have inr : 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (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
ι' : 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)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
inr : 0 ≤ HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
⊢ (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N ≤
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1) *
      HPow.hPow (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)) N
have inr₁ : LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
  (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
⊢ LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have inr : LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
  (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
Tactic: grw [← HH₂, ← le_max_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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)
v : (↑nonarchAbsVal : Type u_4)
j : ι'
inr :
  LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
inr₁ : ι'
⊢ LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
    (⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have inr₂ : LE.le (α := ℝ) (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
  (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j)))
Tactic: grw [← HH₂, ← le_max_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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
⊢ log (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
    log (max (mulHeightBound p) 1) + (↑N : ℝ) * log (mulHeight x)
have pull : log (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
  log (max (mulHeightBound p) 1 * mulHeight x ^ N)
Tactic: pull (disch := positivity) log
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
M N : ℕ
q : ι × ι' → MvPolynomial ι K
inst_2 : IsEmpty ι'
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
⊢ x = 0
have h₁ : ∀ (i : ι), x i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
M N : ℕ
q : ι × ι' → MvPolynomial ι K
inst_2 : IsEmpty ι'
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
i : ι
⊢ x i = 0 i
have h₁ : ∀ (k : ι), 0 = x k ^ (M + N)
Tactic: simp only [Finset.univ_eq_empty, Finset.sum_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have inl : IsEmpty ι' →
  (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
Tactic: rcases isEmpty_or_nonempty ι'
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
inl :
  IsEmpty ι' →
    (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have inr : Nonempty ι' →
  (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
Tactic: rcases isEmpty_or_nonempty ι'
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : IsEmpty ι'
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have inl : (HPow.hPow (α := ℝ) 0 (totalWeight K))⁻¹ ≤ 1
Tactic: simp [show q = 0 from Subsingleton.elim .., max_mulHeightBound_zero_one_eq_one K ι (ι × ι'),
      mulHeight_eval_ge_aux p h]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
q' : ι × ι' → K := fun (a : ι × ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (q a)
⊢ mulHeight x ^ (M + N) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have rw : mulHeight (x ^ (M + N)) ≤
  HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
Tactic: rw [← mulHeight_pow x (M + N)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
q' : ι × ι' → K := fun (a : ι × ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (q a)
⊢ mulHeight (x ^ (M + N)) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have this : x ^ (M + N) = fun (k : ι) ↦
  ∑ j : ι',
    HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
      ((eval x : (a : MvPolynomial ι K) → K) (p j) : K)
Tactic: have : x ^ (M + N) = fun k ↦ ∑ j, (q (k, j)).eval x * (p j).eval x := funext fun k ↦ (h k).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
q' : ι × ι' → K := fun (a : ι × ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (q a)
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have H : mulHeight x ^ (M + N) ≤
  HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
Tactic: have H : mulHeight x ^ (M + N) ≤
      Nat.card ι' ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (p j).eval x := by
    rw [← mulHeight_pow x (M + N)]
    have : x ^ (M + N) = fun k ↦ ∑ j, (q (k, j)).eval x * (p j).eval x := funext fun k ↦ (h k).symm
    simpa [this] using mulHeight_linearMap_apply_le q' _
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
q' : ι × ι' → K := fun (a : ι × ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (q a)
H :
  mulHeight x ^ (M + N) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have inr : mulHeight x ^ N * mulHeight x ^ M ≤
  (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1 *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
    mulHeight x ^ M
Tactic: rw [inv_mul_le_iff₀ ?hC, ← mul_le_mul_iff_left₀ (by positivity : 0 < mulHeight x ^ M)]