awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ι'
inl : (HPow.hPow (α := ℝ) 0 (totalWeight K))⁻¹ ≤ 1
⊢ (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:
simp [show q = 0 from Subsingleton.elim .., max_mulHeightBound_zero_one_eq_one K ι (ι × ι'),
      mulHeight_eval_ge_aux p h]

Premises used: _private.0.Height.mulHeight_eval_ge_aux, Prod, Subsingleton.elim, OfNat.ofNat, Height.max_mulHeightBound_zero_one_eq_one
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 (α := ℝ) 0 (totalWeight K))⁻¹ ≤ 1

Tactic:
grind [zero_pow_eq]

Premises used: zero_pow_eq
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
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)
⊢ 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)]

Premises used: Height.mulHeight_pow, HAdd.hAdd
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
⊢ 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
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
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)
⊢ 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:
simpa [this] using mulHeight_linearMap_apply_le q' _

Premises used: Height.mulHeight_linearMap_apply_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)

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' _
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
⊢ 0 < mulHeight x ^ M

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
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
rw : 0 < HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1
⊢ (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:
rw [inv_mul_le_iff₀ ?hC, ← mul_le_mul_iff_left₀ (by positivity : 0 < mulHeight x ^ M)]

Premises used: inv_mul_le_iff₀, mul_le_mul_iff_left₀
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
⊢ 0 < max (mulHeightBound q) 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
⊢ 0 < HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1

Tactic:
exact mul_pos (mod_cast Nat.one_le_pow _ _ Nat.card_pos) <| by positivity

Premises used: mul_pos
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
⊢ 0 < HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1

Tactic:
case hC => exact mul_pos (mod_cast Nat.one_le_pow _ _ Nat.card_pos) <| by positivity

Premises used: mul_pos
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
inr :
  mulHeight x ^ (M + N) ≤
    (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
⊢ 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 [← pow_add, add_comm]

Premises used: pow_add, add_comm
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
inr :
  (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * (max (mulHeightBound q) 1 * mulHeight x ^ M) *
      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.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
      mulHeight x ^ M
⊢ mulHeight x ^ (M + N) ≤
    (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:
grw [H, mulHeight_eval_le hq x]

Premises used: Height.mulHeight_eval_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ^ M) *
      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.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
      mulHeight x ^ M

Tactic:
ring
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ^ M) *
      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.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
      mulHeight x ^ M

Tactic:
exact Eq.le (by ring)

Premises used: Eq.le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
inl :
  IsEmpty ι' →
    ∃ C > 0,
      ∀ (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)),
        C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
inr :
  Nonempty ι' →
    ∃ C > 0,
      ∀ (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)),
        C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
⊢ ∃ C > 0,
    ∀ (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)),
      C * 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 ι'

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
h_1 : 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)
⊢ 1 * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)

Tactic:
simp [mulHeight_eval_ge_aux p h]

Premises used: _private.0.Height.mulHeight_eval_ge_aux
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
h : IsEmpty ι'
⊢ ∃ C > 0,
    ∀ (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)),
      C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)

Tactic:
exact ⟨1, zero_lt_one, fun p _ h ↦ by simp [mulHeight_eval_ge_aux p h]⟩
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
h : Nonempty ι'
⊢ 0 < Nat.card ι'

Tactic:
have : 0 < Nat.card ι' := Nat.card_pos
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
h : Nonempty ι'
this : 0 < Nat.card ι'
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ > 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
h : Nonempty ι'
this : 0 < Nat.card ι'
⊢ ∃ C > 0,
    ∀ (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)),
      C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)

Tactic:
exact ⟨_, by positivity, mulHeight_eval_ge hq⟩
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ι' →
    -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
        (↑N : ℝ) * log (mulHeight x) ≤
      log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
inr :
  Nonempty ι' →
    -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
        (↑N : ℝ) * log (mulHeight x) ≤
      log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
⊢ -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))

Tactic:
rcases isEmpty_or_nonempty ι'

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ι'
⊢ -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))

Tactic:
simp [show q = 0 from Subsingleton.elim .., mulHeight_eval_ge_aux p h,
      max_mulHeightBound_zero_one_eq_one K ι (ι × ι')]

Premises used: _private.0.Height.mulHeight_eval_ge_aux, Prod, Subsingleton.elim, OfNat.ofNat, Height.max_mulHeightBound_zero_one_eq_one
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ι'
⊢ HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) ≠ 0

Tactic:
simp