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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
⊢ ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr : ∀ (j : ι'),
  (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
Tactic: refine ciSup_le fun j ↦ ?_
-- 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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
⊢ (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr : ∑ i : ι, (v : (a : K) → ℝ) (A (j, i) * x i) ≤
  HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
    ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
Tactic: grw [v.sum_le]
-- 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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
⊢ ∑ i : ι, (v : (a : K) → ℝ) (A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr : ∑ x_1 : ι, HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, x_1)) : ℝ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ≤
  HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
    ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
Tactic: simp only [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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
⊢ ∑ x_1 : ι, HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, x_1)) : ℝ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr : ∑ i : ι, HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
  HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
    ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
Tactic: grw [Finset.sum_le_sum (g := fun _ ↦ (⨆ ji, v (A ji)) * ⨆ i, v (x i)) fun i _ ↦ ?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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
inr :
  ∑ i : ι, HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
⊢ ∑ x_1 : ι, HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, x_1)) : ℝ) ((v : (a : K) → ℝ) (x x_1) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have grw : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
      (fun (x_2 : ι) ↦
          HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)))
        i
Tactic: grw [Finset.sum_le_sum (g := fun _ ↦ (⨆ ji, v (A ji)) * ⨆ i, v (x i)) fun i _ ↦ ?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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have b0 : LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))
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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
b0 : LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have h₁ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)
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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
b0 : LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))
h₁ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have h₂ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
⊢ ∑ i : ι, HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr : Finset.card.{u_2} (α := ι) Finset.univ •
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
  HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
    ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_assoc, Finset.card_univ, Nat.card_eq_fintype_card]
-- 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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
inr :
  Finset.card.{u_2} (α := ι) Finset.univ •
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
⊢ ∑ i : ι, HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr₁ : (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℝ) *
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
  HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
    ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_assoc, Finset.card_univ, Nat.card_eq_fintype_card]
-- 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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
inr :
  Finset.card.{u_2} (α := ι) Finset.univ •
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
inr₁ :
  (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
⊢ ∑ i : ι, HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr₂ : (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℝ) *
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
  (↑(Nat.card ι) : ℝ) *
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_assoc, Finset.card_univ, Nat.card_eq_fintype_card]
-- 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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
inr :
  Finset.card.{u_2} (α := ι) Finset.univ •
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
inr₁ :
  (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
inr₂ :
  (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    (↑(Nat.card ι) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ ∑ i : ι, HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr₃ : (↑(Fintype.card ι) : ℝ) *
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
  (↑(Nat.card ι) : ℝ) *
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_assoc, Finset.card_univ, Nat.card_eq_fintype_card]
-- 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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h : Nonempty ι'
j : ι'
inr :
  Finset.card.{u_2} (α := ι) Finset.univ •
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
inr₁ :
  (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
inr₂ :
  (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    (↑(Nat.card ι) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
inr₃ :
  (↑(Fintype.card ι) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    (↑(Nat.card ι) : ℝ) *
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ ∑ i : ι, HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
have inr₄ : (↑(Fintype.card ι) : ℝ) *
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) ≤
  (↑(Fintype.card ι) : ℝ) *
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_assoc, Finset.card_univ, Nat.card_eq_fintype_card]
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
⊢ ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inl : IsEmpty ι →
  ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rcases isEmpty_or_nonempty ι
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
inl :
  IsEmpty ι →
    ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : Nonempty ι →
  ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rcases isEmpty_or_nonempty ι
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
⊢ ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : IsEmpty ι' →
  ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rcases isEmpty_or_nonempty ι'
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
inr :
  IsEmpty ι' →
    ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
      HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr₁ : Nonempty ι' →
  ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rcases isEmpty_or_nonempty ι'
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
⊢ ⨆ (j : ι'), (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : ∀ (j : ι'),
  (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: refine ciSup_le fun j ↦ ?_
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
⊢ (v : (a : K) → ℝ) (∑ i : ι, A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : ⨆ (i : ↥Finset.univ), (v : (a : K) → ℝ) (A (j, (↑i : ι)) * x (↑i : ι)) ≤
  HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: grw [hv.apply_sum_le]
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
⊢ ⨆ (i : ↥Finset.univ), (v : (a : K) → ℝ) (A (j, (↑i : ι)) * x (↑i : ι)) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : ⨆ (i : ↥Finset.univ),
    HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, (↑i : ι))) : ℝ) ((v : (a : K) → ℝ) (x (↑i : ι)) : ℝ) ≤
  HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: simp only [map_mul]
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
⊢ ⨆ (i : ↥Finset.univ),
      HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, (↑i : ι))) : ℝ) ((v : (a : K) → ℝ) (x (↑i : ι)) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
Tactic: have (f : ι → ℝ) : ⨆ i : ↥Finset.univ, f i.val = ⨆ i, f i :=
    Function.Surjective.iSup_comp (fun i ↦ ⟨⟨i, Finset.mem_univ i⟩, rfl⟩) f
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
⊢ ⨆ (i : ↥Finset.univ),
      HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, (↑i : ι))) : ℝ) ((v : (a : K) → ℝ) (x (↑i : ι)) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : ⨆ (i : ι), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
  HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: rw [this fun i ↦ v (A (j, i)) * v (x i)]
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
⊢ ⨆ (i : ι), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : ∀ (i : ι),
  HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: refine ciSup_le fun i ↦ ?_
-- 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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr : LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))
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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
inr : LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr₁ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)
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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean (R := ℝ) (α := K) (⇑v : (a : K) → ℝ)
A : ι' × ι → K
x : ι → K
h : Nonempty ι
h_1 : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), Eq (α := ℝ) (⨆ (i : ↥Finset.univ), f (↑i : ι)) (⨆ (i : ι), f i)
i : ι
inr : LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))
inr₁ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) ≤
    HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have inr₂ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (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
⊢ 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have rw : HMul.hMul (α := ℝ) 1 1 * 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
Tactic: rw [show (1 : ℝ) = 1 * 1 * 1 by ring]
-- 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
⊢ HMul.hMul (α := ℝ) 1 1 * 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K) * mulHeight A * mulHeight x
have h₁ : 1 ≤ HPow.hPow (α := ℝ) (↑(Nat.card ι) : ℝ) (totalWeight K)
Tactic: gcongr