awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddCommMonoid β
inst_1 : FunLike F β ℝ
inst_2 : NonnegHomClass F β ℝ
inst_3 : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean.{0, u_3} (R := ℝ) (α := β) (⇑v : (a : β) → ℝ)
a : α
s : Finset α
ha : a ∉ s
ih : LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
hs : Nonempty.{u_2 + 1} ↥s
⊢ LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))

Tactic:
exact ciSup_le fun i ↦ Finite.le_ciSup_of_le (⟨i.val, Finset.mem_insert_of_mem i.prop⟩) le_rfl

Premises used: Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddCommMonoid β
inst_1 : FunLike F β ℝ
inst_2 : NonnegHomClass F β ℝ
inst_3 : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean.{0, u_3} (R := ℝ) (α := β) (⇑v : (a : β) → ℝ)
s : Finset α
empty : LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ ∅, l i) : ℝ) (⨆ (i : ↥∅), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ih : LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)),
    LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ Insert.insert a s, l i) : ℝ)
      (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.sum_insert ha]
    grw [hv .., ih]
    refine max_le ?_ ?_
    · exact Finite.le_ciSup_of_le ⟨_, s.mem_insert_self a⟩ le_rfl
    · rcases isEmpty_or_nonempty s with hs | hs
      · simpa using Real.iSup_nonneg_of_nonnegHomClass v _
      exact ciSup_le fun i ↦ Finite.le_ciSup_of_le (⟨i.val, Finset.mem_insert_of_mem i.prop⟩) le_rfl

Premises used: le_rfl, Membership.mem, isEmpty_or_nonempty, Subtype, Insert.insert, Finite.le_ciSup_of_le, max_le, Real.iSup_nonneg_of_nonnegHomClass, ciSup_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddCommMonoid β
inst_1 : FunLike F β ℝ
inst_2 : NonnegHomClass F β ℝ
inst_3 : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean.{0, u_3} (R := ℝ) (α := β) (⇑v : (a : β) → ℝ)
s : Finset α
empty : LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ ∅, l i) : ℝ) (⨆ (i : ↥∅), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ih : LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)),
    LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ Insert.insert a s, l i) : ℝ)
      (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.sum_insert ha]
    grw [hv .., ih]
    refine max_le ?_ ?_
    · exact Finite.le_ciSup_of_le ⟨_, s.mem_insert_self a⟩ le_rfl
    · rcases isEmpty_or_nonempty s with hs | hs
      · simpa using Real.iSup_nonneg_of_nonnegHomClass v _
      exact ciSup_le fun i ↦ Finite.le_ciSup_of_le (⟨i.val, Finset.mem_insert_of_mem i.prop⟩) le_rfl

Premises used: le_rfl, Membership.mem, isEmpty_or_nonempty, Subtype, Insert.insert, Finite.le_ciSup_of_le, max_le, Real.iSup_nonneg_of_nonnegHomClass, ciSup_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddCommMonoid β
inst_1 : FunLike F β ℝ
inst_2 : NonnegHomClass F β ℝ
inst_3 : ZeroHomClass F β ℝ
v : F
l : α → β
inst_4 : Fintype α
hv : IsNonarchimedean.{0, u_3} (R := ℝ) (α := β) (⇑v : (a : β) → ℝ)
⊢ ∀ (i : α), Membership.mem (γ := Finset α) Finset.univ i

Tactic:
grind
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddCommMonoid β
inst_1 : FunLike F β ℝ
inst_2 : NonnegHomClass F β ℝ
inst_3 : ZeroHomClass F β ℝ
v : F
l : α → β
inst_4 : Fintype α
hv : IsNonarchimedean.{0, u_3} (R := ℝ) (α := β) (⇑v : (a : β) → ℝ)
grw :
  LE.le (α := ℝ)
    (⨆ (i : α),
      ⨆ (h : Membership.mem (γ := Finset α) Finset.univ i),
        (v : (a : β) → ℝ) (l (↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) Finset.univ x) i h) : α)))
    (⨆ (i : α), (v : (a : β) → ℝ) (l i))
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i : α, l i) : ℝ) (⨆ (i : α), (v : (a : β) → ℝ) (l i) : ℝ)

Tactic:
grw [hv.apply_sum_le, ← cbiSup_eq_of_forall (by grind)]

Premises used: cbiSup_eq_of_forall, IsNonarchimedean.apply_sum_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddCommMonoid β
inst_1 : FunLike F β ℝ
inst_2 : NonnegHomClass F β ℝ
inst_3 : ZeroHomClass F β ℝ
v : F
l : α → β
inst_4 : Fintype α
hv : IsNonarchimedean.{0, u_3} (R := ℝ) (α := β) (⇑v : (a : β) → ℝ)
⊢ LE.le (α := ℝ)
    (⨆ (i : α),
      ⨆ (h : Membership.mem (γ := Finset α) Finset.univ i),
        (v : (a : β) → ℝ) (l (↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) Finset.univ x) i h) : α)))
    (⨆ (i : α), (v : (a : β) → ℝ) (l i))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
inl :
  IsEmpty ι' →
    ⨆ (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)
inr :
  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)
⊢ ⨆ (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:
rcases isEmpty_or_nonempty ι'

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 : IsEmpty ι'
⊢ ⨆ (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:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)

Tactic:
ciSup_le fun j ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ι'
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)
⊢ ⨆ (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 ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 : ι, (v : (a : K) → ℝ) (A (j, i) * x i) ≤
    HMul.hMul (α := ℝ) (↑(Nat.card ι) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) *
      ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
⊢ (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:
grw [v.sum_le]

Premises used: AbsoluteValue.sum_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 :
  ∑ 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)
⊢ ∑ 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:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
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
⊢ ∑ 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:
grw [Finset.sum_le_sum (g := fun _ ↦ (⨆ ji, v (A ji)) * ⨆ i, v (x i)) fun i _ ↦ ?h]

Premises used: Finset.sum_le_sum
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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) : ℝ)
h₂ : LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x 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:
gcongr
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))

Tactic:
Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ LE.le (α := ℝ) 0 (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji))

Tactic:
exact Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)

Tactic:
Finite.le_ciSup_of_le (j, i) le_rfl

Premises used: le_rfl, Prod.mk, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (A (j, i)) : ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le (j, i) le_rfl

Premises used: le_rfl, Prod.mk, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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) : ℝ) ≤
    (fun (x_1 : ι) ↦
        HMul.hMul (α := ℝ) (⨆ (ji : ι' × ι), (v : (a : K) → ℝ) (A ji)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)))
      i

Tactic:
case h =>
    dsimp only
    gcongr
    · exact Real.iSup_nonneg_of_nonnegHomClass v _
    · exact Finite.le_ciSup_of_le (j, i) le_rfl
    · exact Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Prod.mk, Finite.le_ciSup_of_le, Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))
inr₄ 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))
⊢ ∑ 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:
rw [Finset.sum_const, nsmul_eq_mul, mul_assoc, Finset.card_univ, Nat.card_eq_fintype_card]

Premises used: Finset.card_univ, mul_assoc, nsmul_eq_mul, Nat.card_eq_fintype_card, Finset.sum_const
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))
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))
⊢ ⨆ (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 ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 : 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:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))
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))
⊢ ⨆ (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 ι'

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

Tactic:
ciSup_le fun j ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ι'
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))
⊢ ⨆ (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 ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 : ι'
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))
⊢ (v : (a : K) → ℝ) (∑ i : ι, 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]

Premises used: IsNonarchimedean.apply_sum_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 : ι'
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))
⊢ ⨆ (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:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 : ι'
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)
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))
⊢ ⨆ (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:
rw [this fun i ↦ v (A (j, i)) * v (x i)]

Premises used: HMul.hMul, Prod.mk, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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))

Tactic:
ciSup_le fun i ↦ ?_

Premises used: ciSup_le