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)
⊢ HMul.hMul (α := ℝ) 1 1 * 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have h₂ : 1 ≤ mulHeight A
Tactic: gcongr
-- 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)
h₂ : 1 ≤ mulHeight A
⊢ HMul.hMul (α := ℝ) 1 1 * 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have h₃ : 1 ≤ mulHeight x
Tactic: gcongr
-- 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
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
Tactic: have H₀ : 1 ≤ Nat.card ι ^ totalWeight K * mulHeight A * mulHeight x := by
    rw [show (1 : ℝ) = 1 * 1 * 1 by ring]
    gcongr
    · exact_mod_cast Nat.one_le_pow _ _ Nat.card_pos
    · exact one_le_mulHeight _
    · exact one_le_mulHeight _
-- 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
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inl : ∀ (hι' : IsEmpty ι'),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight 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
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
inl :
  ∀ (hι' : IsEmpty ι'),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr : ∀ (hι' : Nonempty ι'),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight 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
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr : ∀ (h : Eq (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
Tactic: rcases eq_or_ne (fun j ↦ ∑ i, A (j, i) * x i) 0 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
inst_4 : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
hι' : Nonempty ι'
inr :
  ∀ (h : Eq (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr₁ : ∀ (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) 0),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
Tactic: rcases eq_or_ne (fun j ↦ ∑ i, A (j, i) * x i) 0 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
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
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr : ∀ (H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x)
  (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) 0),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x
Tactic: rcases eq_or_ne A 0 with rfl | hA
Cleared hypotheses: A, 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
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
inr :
  ∀ (H₀ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x)
    (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, 0 (j, i) * x i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight (K := K) (ι := ι' × ι) 0 * mulHeight x
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr₁ : ∀ (hA : A ≠ 0),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
Tactic: rcases eq_or_ne A 0 with rfl | hA
-- 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
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr : ∀
  (H₀ :
    1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0)
  (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) 0),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x, 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
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
inr :
  ∀
    (H₀ :
      1 ≤
        HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0)
    (h : Ne (α := (j : ι') → K) (fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) 0),
    (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * 0 i) ≤
      HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr₁ : ∀ (hx : x ≠ 0),
  (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- 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
⊢ (mulHeight.{u_1, u_3} (K := K) fun (j : ι') ↦ ∑ i : ι, A (j, i) * x i) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have inr : HMul.hMul (α := ℝ)
    (prod
      (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) ≤
  HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal) *
    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))
Tactic: rw [mulHeight_eq h, mulHeight_eq hA, mulHeight_eq hx, mul_mul_mul_comm, ← mul_assoc, ← mul_assoc,
    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
⊢ HMul.hMul (α := ℝ)
      (prod
        (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
          prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal) *
      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 (α := ℝ) 0
  (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
    ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))
Tactic: gcongr
-- 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
inr :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))
⊢ HMul.hMul (α := ℝ)
      (prod
        (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
          prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal) *
      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₁ : 0 ≤
  HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
    prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
Tactic: gcongr
-- 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
inr :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))
inr₁ :
  0 ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
⊢ HMul.hMul (α := ℝ)
      (prod
        (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
          prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal) *
      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₂ : prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal) ≤
  HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
    prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
Tactic: gcongr
-- 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
inr :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1))
inr₁ :
  0 ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
inr₂ :
  prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
⊢ HMul.hMul (α := ℝ)
      (prod
        (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
          prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal) *
      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₃ : ∏ᶠ (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))
Tactic: gcongr
-- 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
⊢ 0 ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
have inr : LE.le (α := ℝ) 0 (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
Tactic: refine mul_nonneg (mul_nonneg (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
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
inr : LE.le (α := ℝ) 0 (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
⊢ 0 ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
have inr₁ : LE.le (α := ℝ) 0 (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal))
Tactic: refine mul_nonneg (mul_nonneg (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
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
⊢ prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) *
        prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal) *
      prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι' × ι), (v : (a : K) → ℝ) (A i)) archAbsVal)
have inr : LE.le (α := ℝ)
  (prod (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
  (prod
    (map
      (fun (i : AbsoluteValue K ℝ) ↦
        (↑(Nat.card ι) : ℝ) *
          HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι' × ι), (i : (a : K) → ℝ) (A i_1)))
      archAbsVal))
Tactic: rw [mul_assoc, ← prod_map_mul, ← prod_replicate, totalWeight, ← map_const', ← prod_map_mul]
-- 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 (α := ℝ)
    (prod
      (map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (∑ i_1 : ι, A (i, i_1) * x i_1)) archAbsVal))
    (prod
      (map
        (fun (i : AbsoluteValue K ℝ) ↦
          (↑(Nat.card ι) : ℝ) *
            HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι' × ι), (i : (a : K) → ℝ) (A i_1)))
        archAbsVal))
have inr : ∀ (v : AbsoluteValue K ℝ),
  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))
Tactic: refine prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _) fun v _ ↦ ?_