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
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 : ℕ)) : ℝ)
inr : LE.le (α := ℝ) 0 (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p))
⊢ 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 (α := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ) (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p) : ℝ)
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 ℝ
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 : ℕ)) : ℝ)
inr : LE.le (α := ℝ) 0 (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p))
inr₁ :
  LE.le (α := ℝ) ((v : (a : K) → ℝ) (coeff s p) : ℝ) (⨆ (s : ↥p.support), (v : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) p) : ℝ)
⊢ 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₂ : ∏ 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 ℝ
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 : ℕ)) : ℝ)
⊢ ∏ 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 inr : 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 ℝ
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 : ℕ)) : ℝ)
⊢ 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 inr : ∀ 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
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
⊢ max (mulHeightBound.{u_4, u_5, u_6} (K := K) (ι := ι) (ι' := ι') 0) 1 = 1
have simp : max
    (HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum 0 fun (x_1 : ι →₀ ℕ) (c : K) ↦ (x : (a : K) → ℝ) c)
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
    1 =
  1
Tactic: simp only [mulHeightBound_eq, Pi.zero_apply, support_zero, coeff_zero, AbsoluteValue.map_zero,
    Real.iSup_of_isEmpty, zero_le_one, sup_of_le_right]
-- 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
⊢ max
      (HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), 0) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have simp : max
    (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
    1 =
  1
Tactic: simp only [Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate, zero_pow_eq]
-- 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
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have inl : IsEmpty ι' →
  max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
Tactic: rcases isEmpty_or_nonempty ι'
-- 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
inl :
  IsEmpty ι' →
    max
        (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
          (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
        1 =
      1
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have inr : Nonempty ι' →
  max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
Tactic: rcases isEmpty_or_nonempty ι'
-- 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
h : IsEmpty ι'
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have pos : Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 →
  max (HMul.hMul (α := ℝ) 1 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1)) 1 = 1
Tactic: split_ifs
-- 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
h : IsEmpty ι'
pos :
  Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 →
    max (HMul.hMul (α := ℝ) 1 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1)) 1 = 1
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have neg : ¬Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 →
  max (HMul.hMul (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1)) 1 = 1
Tactic: split_ifs
-- 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
h : Nonempty ι'
⊢ max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have inr : LE.le (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0) 1
Tactic: simp
-- 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
⊢ max
      (HMul.hMul (α := ℝ)
        (Multiset.prod
          (Multiset.map
            (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum 0 fun (x_1 : ι →₀ ℕ) (c : K) ↦ (x : (a : K) → ℝ) c)
            archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have set_option : max
    (HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), 0) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
    1 =
  1
Tactic: set_option backward.isDefEq.respectTransparency false in -- temporary measure
  simp only [Finsupp.sum_zero_index] -- singling this out for needing the above
  simp only [Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate, zero_pow_eq]
  rcases isEmpty_or_nonempty ι'
  · split_ifs
    · simpa using finprod_zero_le_one
    · simp
  · simp
    grind
-- 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
set_option :
  max
      (HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), 0) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
⊢ max
      (HMul.hMul (α := ℝ)
        (Multiset.prod
          (Multiset.map
            (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum 0 fun (x_1 : ι →₀ ℕ) (c : K) ↦ (x : (a : K) → ℝ) c)
            archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have set_option₁ : max
    (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
    1 =
  1
Tactic: set_option backward.isDefEq.respectTransparency false in -- temporary measure
  simp only [Finsupp.sum_zero_index] -- singling this out for needing the above
  simp only [Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate, zero_pow_eq]
  rcases isEmpty_or_nonempty ι'
  · split_ifs
    · simpa using finprod_zero_le_one
    · simp
  · simp
    grind
-- 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
set_option :
  max
      (HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), 0) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
set_option₁ :
  max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
⊢ max
      (HMul.hMul (α := ℝ)
        (Multiset.prod
          (Multiset.map
            (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum 0 fun (x_1 : ι →₀ ℕ) (c : K) ↦ (x : (a : K) → ℝ) c)
            archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have inl : IsEmpty ι' →
  max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
Tactic: set_option backward.isDefEq.respectTransparency false in -- temporary measure
  simp only [Finsupp.sum_zero_index] -- singling this out for needing the above
  simp only [Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate, zero_pow_eq]
  rcases isEmpty_or_nonempty ι'
  · split_ifs
    · simpa using finprod_zero_le_one
    · simp
  · simp
    grind
-- 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
set_option :
  max
      (HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), 0) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
set_option₁ :
  max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
inl :
  IsEmpty ι' →
    max
        (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
          (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
        1 =
      1
⊢ max
      (HMul.hMul (α := ℝ)
        (Multiset.prod
          (Multiset.map
            (fun (x : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum 0 fun (x_1 : ι →₀ ℕ) (c : K) ↦ (x : (a : K) → ℝ) c)
            archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
have inr : Nonempty ι' →
  max
      (HMul.hMul (α := ℝ) (if Multiset.card.{u_4} (α := AbsoluteValue K ℝ) archAbsVal = 0 then 1 else 0)
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)), ⨆ (j : ι'), 1))
      1 =
    1
Tactic: set_option backward.isDefEq.respectTransparency false in -- temporary measure
  simp only [Finsupp.sum_zero_index] -- singling this out for needing the above
  simp only [Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate, zero_pow_eq]
  rcases isEmpty_or_nonempty ι'
  · split_ifs
    · simpa using finprod_zero_le_one
    · simp
  · simp
    grind
-- 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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
have refine : ∀ (j : ι'),
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
Tactic: refine HasFiniteMulSupport.iSup 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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
have inl : ∀ (hs₀ : IsEmpty.{u_5 + 1} ↥(p j).support),
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
Tactic: rcases isEmpty_or_nonempty (p j).support with hs₀ | hs₀
-- 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 ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
inl :
  ∀ (hs₀ : IsEmpty.{u_5 + 1} ↥(p j).support),
    HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
      max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
have inr : ∀ (hs₀ : Nonempty.{u_5 + 1} ↥(p j).support),
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
Tactic: rcases isEmpty_or_nonempty (p j).support with hs₀ | hs₀
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
ι : Type u_5
ι' : Type u_6
inst_1 : AdmissibleAbsValues K
inst_2 : Finite ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : Nonempty.{u_5 + 1} ↥(p j).support
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_4)) ↦
    max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1
have H : ∀ (s : ↥(p j).support), coeff (↑s : ι →₀ ℕ) (p j) ≠ 0
Tactic: have H (s : (p j).support) : coeff s.val (p j) ≠ 0 := mem_support_iff.mp s.prop
-- 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ (mulHeight.{u_4, u_6} (K := K) fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) ≤ mulHeightBound p
have simp : HMul.hMul (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦
          ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
        archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K)) ≤
  HMul.hMul (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
        archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
Tactic: simp only [mulHeight_eq h, mulHeightBound_eq]
-- 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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦
            ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K)) ≤
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have c0 : LE.le (α := ℝ) 0
  (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
c0 :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦
            ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K)) ≤
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have b0 : 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))
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 ι'
p : ι' → MvPolynomial ι K
h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ (constantCoeff : (a : MvPolynomial ι K) → K) (p j)) 0
c0 :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
b0 :
  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))
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦
            ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K)) ≤
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_4)),
        ⨆ (j : ι'),
          max (⨆ (s : ↥(p j).support), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (coeff (↑s : ι →₀ ℕ) (p j))) 1)
have h₁ : LE.le (α := ℝ)
  (Multiset.prod
    (Multiset.map
      (fun (v : AbsoluteValue K ℝ) ↦
        ⨆ (i : ι'), (v : (a : K) → ℝ) ((constantCoeff : (a : MvPolynomial ι K) → K) (p i) : K))
      archAbsVal))
  (Multiset.prod
    (Multiset.map
      (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) ↦ (v : (a : K) → ℝ) c)
      archAbsVal))
Tactic: gcongr