awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
v : AbsoluteValue R S
hv : IsNonarchimedean.{u_2, u_1} (R := S) (α := R) (⇑v : (a : R) → S)
ι : Type u_3
s : Finset ι
x : ι → R
hs : s.Nonempty
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) (∑ i ∈ s, x i) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)
have inr : LE.le.{u_2} (α := S) (s.sup' hs fun (i : ι) ↦ (v : (a : R) → S) (x i)) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
Tactic: grw [hv.apply_sum_le_sup hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ HMul.hMul (α := ℝ)
      (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) ≤
    HPow.hPow (α := ℝ) (↑(#s) : ℝ) (Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal) *
      ∏ x_1 ∈ s,
        HMul.hMul (α := ℝ)
          (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (x x_1)) 1) archAbsVal))
          (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x x_1)) 1)
have rw : HMul.hMul (α := ℝ)
    (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) ≤
  HMul.hMul (α := ℝ)
    (prod
      (Multiset.map
        (fun (i : AbsoluteValue K ℝ) ↦
          HMul.hMul (α := ℝ) (Function.const (AbsoluteValue K ℝ) (↑(#s) : ℝ) i)
            (∏ a ∈ s, max ((i : (a : K) → ℝ) (x a)) 1))
        archAbsVal))
    (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ∏ b ∈ s, max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1)
Tactic: rw [prod_mul_distrib, ← prod_replicate, ← map_const, ← finprod_prod_comm _ _ (by fun_prop),
    ← prod_map_prod, ← mul_assoc, ← prod_map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ HMul.hMul (α := ℝ)
      (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) ≤
    HMul.hMul (α := ℝ)
      (prod
        (Multiset.map
          (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
          archAbsVal))
      (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ∏ b ∈ s, max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1)
have c0 : LE.le (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
c0 :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1)
⊢ HMul.hMul (α := ℝ)
      (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) ≤
    HMul.hMul (α := ℝ)
      (prod
        (Multiset.map
          (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
          archAbsVal))
      (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ∏ b ∈ s, max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1)
have b0 : LE.le (α := ℝ) 0
  (prod
    (Multiset.map
      (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
      archAbsVal))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
c0 :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1)
b0 :
  LE.le (α := ℝ) 0
    (prod
      (Multiset.map
        (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
        archAbsVal))
⊢ HMul.hMul (α := ℝ)
      (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) ≤
    HMul.hMul (α := ℝ)
      (prod
        (Multiset.map
          (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
          archAbsVal))
      (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ∏ b ∈ s, max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1)
have h₁ : LE.le (α := ℝ) (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
  (prod
    (Multiset.map
      (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
      archAbsVal))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
c0 :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1)
b0 :
  LE.le (α := ℝ) 0
    (prod
      (Multiset.map
        (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
        archAbsVal))
h₁ :
  LE.le (α := ℝ)
    (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
    (prod
      (Multiset.map
        (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
        archAbsVal))
⊢ HMul.hMul (α := ℝ)
      (prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1) ≤
    HMul.hMul (α := ℝ)
      (prod
        (Multiset.map
          (fun (x_1 : AbsoluteValue K ℝ) ↦ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1))
          archAbsVal))
      (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ∏ b ∈ s, max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1)
have h₂ : LE.le (α := ℝ) (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1)
  (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ∏ b ∈ s, max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
⊢ logHeight₁.{u_1} (K := K) (∑ a ∈ s, x a) ≤ (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ a ∈ s, logHeight₁ (x a)
have inl : logHeight₁.{u_1} (K := K) (∑ a ∈ ∅, x a) ≤
  (↑(totalWeight K) : ℝ) * log (↑(card.{u_2} (α := α) ∅) : ℝ) + ∑ a ∈ ∅, logHeight₁ (x a)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
inl :
  logHeight₁.{u_1} (K := K) (∑ a ∈ ∅, x a) ≤
    (↑(totalWeight K) : ℝ) * log (↑(card.{u_2} (α := α) ∅) : ℝ) + ∑ a ∈ ∅, logHeight₁ (x a)
⊢ logHeight₁.{u_1} (K := K) (∑ a ∈ s, x a) ≤ (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ a ∈ s, logHeight₁ (x a)
have inr : ∀ (hs : s.Nonempty),
  logHeight₁.{u_1} (K := K) (∑ a ∈ s, x a) ≤ (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ a ∈ s, logHeight₁ (x a)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
⊢ log (mulHeight₁.{u_1} (K := K) (∑ a ∈ s, x a)) ≤
    (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ x_1 ∈ s, log (mulHeight₁ (x x_1))
have this : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0
Tactic: have : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0 := fun _ _ ↦ by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
this : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0
⊢ log (mulHeight₁.{u_1} (K := K) (∑ a ∈ s, x a)) ≤
    (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ x_1 ∈ s, log (mulHeight₁ (x x_1))
have this₁ : HPow.hPow (α := ℝ) (↑(#s) : ℝ) (totalWeight K) ≠ 0
Tactic: have : (#s : ℝ) ^ totalWeight K ≠ 0 := by simp [hs.ne_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
this_1 : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0
this : HPow.hPow (α := ℝ) (↑(#s) : ℝ) (totalWeight K) ≠ 0
⊢ log (mulHeight₁.{u_1} (K := K) (∑ a ∈ s, x a)) ≤
    (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ x_1 ∈ s, log (mulHeight₁ (x x_1))
have inr : log (mulHeight₁.{u_1} (K := K) (∑ a ∈ s, x a)) ≤
  log (HPow.hPow (α := ℝ) (↑(#s) : ℝ) (totalWeight K) * ∏ i ∈ s, mulHeight₁ (x i))
Tactic: pull (disch := first | assumption | positivity) log
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (x + y) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ y
have rw : mulHeight₁ (Finset.sum Finset.univ ![x, y]) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * (mulHeight₁ x * mulHeight₁ y)
Tactic: rw [show x + y = Finset.univ.sum ![x, y] by simp, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (Finset.sum Finset.univ ![x, y]) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * (mulHeight₁ x * mulHeight₁ y)
have grw : HPow.hPow (α := ℝ) (↑(Finset.card (α := Fin (Nat.succ 0).succ) Finset.univ) : ℝ) (totalWeight K) *
    ∏ a : Fin (Nat.succ 0).succ, mulHeight₁ (![x, y] a) ≤
  HPow.hPow (α := ℝ) 2 (totalWeight K) * (mulHeight₁ x * mulHeight₁ y)
Tactic: grw [mulHeight₁_sum_le Finset.univ_nonempty ![x, y]]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x + y)) ≤ (↑(totalWeight K) : ℝ) * log 2 + log (mulHeight₁ x) + log (mulHeight₁ y)
have pull : log (mulHeight₁ (x + y)) ≤ log (HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ y)
Tactic: pull (disch := positivity) log
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (x - y) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ y
have rw : mulHeight₁ (x + -y) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ (-y)
Tactic: rw [sub_eq_add_neg, ← mulHeight₁_neg y]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x - y) ≤ (↑(totalWeight K) : ℝ) * log 2 + logHeight₁ x + logHeight₁ y
have rw : logHeight₁ (x + -y) ≤ (↑(totalWeight K) : ℝ) * log 2 + logHeight₁ x + logHeight₁ (-y)
Tactic: rw [sub_eq_add_neg, ← logHeight₁_neg y]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
f : Fin 2 → ℝ
⊢ iSup f = max (f 0) (f 1)
have rw : iSup ![f 0, f 1] = max (![f 0, f 1] 0) (![f 0, f 1] 1)
Tactic: rw [show f = ![f 0, f 1] from List.ofFn_inj.mp rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ insert a s, l i) : ℝ)
    (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have insert : LE.le (α := ℝ) ((v : (a : β) → ℝ) (l a + ∑ x ∈ s, l x) : ℝ) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
Tactic: rw [Finset.sum_insert ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (l a + ∑ x ∈ s, l x) : ℝ)
    (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have insert : LE.le (α := ℝ) (max ((v : (a : β) → ℝ) (l a)) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) : ℝ)
  (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
Tactic: grw [hv .., ih]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
⊢ LE.le (α := ℝ) (max ((v : (a : β) → ℝ) (l a)) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) : ℝ)
    (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have insert : LE.le (α := ℝ) ((v : (a : β) → ℝ) (l a) : ℝ) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
Tactic: refine max_le ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
insert : LE.le (α := ℝ) ((v : (a : β) → ℝ) (l a) : ℝ) (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
⊢ LE.le (α := ℝ) (max ((v : (a : β) → ℝ) (l a)) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) : ℝ)
    (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have insert₁ : LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)))
  (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))
Tactic: refine max_le ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
⊢ LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))
have insert : ∀ (hs : IsEmpty.{u_2 + 1} ↥s),
  LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))
Tactic: rcases isEmpty_or_nonempty s with hs | hs
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
insert :
  ∀ (hs : IsEmpty.{u_2 + 1} ↥s),
    LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)))
      (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))
⊢ LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)))
    (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))
have insert₁ : ∀ (hs : Nonempty.{u_2 + 1} ↥s),
  LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)))
    (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))
Tactic: rcases isEmpty_or_nonempty s with hs | hs
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 α
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have empty : LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ ∅, l i) : ℝ) (⨆ (i : ↥∅), (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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have 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 a s, l i) : ℝ)
    (⨆ (i : ↥(insert a 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 α
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have empty : LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ ∅, l i) : ℝ) (⨆ (i : ↥∅), (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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 : α)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ s, l i) : ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
have 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 a s, l i) : ℝ)
    (⨆ (i : ↥(insert a 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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 (α := ℝ) ((v : (a : β) → ℝ) (∑ i : α, l i) : ℝ) (⨆ (i : α), (v : (a : β) → ℝ) (l i) : ℝ)
have 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))
Tactic: grw [hv.apply_sum_le, ← cbiSup_eq_of_forall (by grind)]
-- 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
⊢ ⨆ (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 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)
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 ℝ
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)
⊢ ⨆ (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 : 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: rcases isEmpty_or_nonempty ι'