awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
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)
⊢ 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)

Tactic:
rw [prod_mul_distrib, ← prod_replicate, ← map_const, ← finprod_prod_comm _ _ (by fun_prop),
    ← prod_map_prod, ← mul_assoc, ← prod_map_mul]

Premises used: Multiset.prod_replicate, Finset.prod_mul_distrib, mul_assoc, Multiset.map_const, Multiset.prod_map_mul, finprod_prod_comm, Multiset.prod_map_prod
-- Module: Mathlib.NumberTheory.Height.Basic
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))
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)
⊢ 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)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
x_1 : (↑nonarchAbsVal : Type u_1)
⊢ LE.le (α := ℝ) (0 : ℝ) (max (((↑x_1 : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1 : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1)

Tactic:
exact finprod_nonneg fun _ ↦ by positivity

Premises used: finprod_nonneg
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
x_1 : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal x_1
⊢ 0 ≤ HMul.hMul (α := ℝ) (↑(#s) : ℝ) (∏ a ∈ s, max ((x_1 : (a : K) → ℝ) (x a)) 1)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 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:
exact prod_map_nonneg fun _ h ↦ by positivity

Premises used: Multiset.prod_map_nonneg
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
x_1 : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal x_1
⊢ LE.le (α := ℝ) (0 : ℝ) (max ((x_1 : (a : K) → ℝ) (∑ a ∈ s, x a)) 1 : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 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:
exact prod_map_le_prod_map₀ _ _ (fun _ _ ↦ by positivity) fun _ _ ↦ max_abv_sum_one_le _ hs x

Premises used: Multiset.prod_map_le_prod_map₀, Finset.max_abv_sum_one_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
x_1 : (↑nonarchAbsVal : Type u_1)
⊢ LE.le (α := ℝ) (0 : ℝ) (max (((↑x_1 : AbsoluteValue K ℝ) : (a : K) → ℝ) (∑ a ∈ s, x a)) 1 : ℝ)

Tactic:
grind
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (a : (↑nonarchAbsVal : Type u_1)) ↦
    ∏ b ∈ s, max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 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:
exact finprod_le_finprod (by fun_prop) (fun _ ↦ by grind) (by fun_prop) <|
      fun v ↦ max_abv_sum_one_le_of_isNonarchimedean (isNonarchimedean _ v.prop) _ x

Premises used: Height.AdmissibleAbsValues.isNonarchimedean, finprod_le_finprod, Finset.max_abv_sum_one_le_of_isNonarchimedean
-- Module: Mathlib.NumberTheory.Height.Basic
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)
inr :
  ∀ (hs : s.Nonempty),
    logHeight₁.{u_1} (K := K) (∑ a ∈ s, x a) ≤ (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ a ∈ s, logHeight₁ (x a)
⊢ 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

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
x : α → K
⊢ logHeight₁.{u_1} (K := K) (∑ a ∈ ∅, x a) ≤
    (↑(totalWeight K) : ℝ) * log (↑(card.{u_2} (α := α) ∅) : ℝ) + ∑ a ∈ ∅, logHeight₁ (x a)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
x_1 : α
h : x_1 ∈ s
⊢ mulHeight₁ (x x_1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
⊢ ∀ a ∈ s, mulHeight₁ (x a) ≠ 0

Tactic:
have : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0 := fun _ _ ↦ by positivity
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (totalWeight K) ≠ 0

Tactic:
simp [hs.ne_empty]

Premises used: Finset.Nonempty.ne_empty
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (totalWeight K) ≠ 0

Tactic:
have : (#s : ℝ) ^ totalWeight K ≠ 0 := by simp [hs.ne_empty]
-- Module: Mathlib.NumberTheory.Height.Basic
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
inr :
  log (mulHeight₁.{u_1} (K := K) (∑ a ∈ s, x a)) ≤
    log (HPow.hPow (α := ℝ) (↑(#s) : ℝ) (totalWeight K) * ∏ i ∈ s, mulHeight₁ (x i))
⊢ log (mulHeight₁.{u_1} (K := K) (∑ a ∈ s, x a)) ≤
    (↑(totalWeight K) : ℝ) * log (↑(#s) : ℝ) + ∑ x_1 ∈ s, log (mulHeight₁ (x x_1))

Tactic:
pull (disch := first | assumption | positivity) log

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ 0 < mulHeight₁.{u_1} (K := K) (∑ a ∈ s, x a)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.Basic
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)) ≤
    log (HPow.hPow (α := ℝ) (↑(#s) : ℝ) (totalWeight K) * ∏ i ∈ s, mulHeight₁ (x i))

Tactic:
exact (log_le_log <| by positivity) <| mulHeight₁_sum_le hs x

Premises used: Height.mulHeight₁_sum_le, Real.log_le_log
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ (-x) = mulHeight₁ x

Tactic:
simp [mulHeight₁_eq]

Premises used: Height.mulHeight₁_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ logHeight₁ (-x) = logHeight₁ x

Tactic:
simp [logHeight₁_eq_log_mulHeight₁, mulHeight₁_neg]

Premises used: Height.logHeight₁_eq_log_mulHeight₁, Height.mulHeight₁_neg
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ x + y = Finset.sum Finset.univ ![x, y]

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
rw : mulHeight₁ (Finset.sum Finset.univ ![x, y]) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * (mulHeight₁ x * mulHeight₁ y)
⊢ mulHeight₁ (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]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
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)
⊢ mulHeight₁ (Finset.sum Finset.univ ![x, y]) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * (mulHeight₁ x * mulHeight₁ y)

Tactic:
grw [mulHeight₁_sum_le Finset.univ_nonempty ![x, y]]

Premises used: Finset.univ_nonempty, Height.mulHeight₁_sum_le, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ 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:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
pull : log (mulHeight₁ (x + y)) ≤ log (HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ y)
⊢ log (mulHeight₁ (x + y)) ≤ (↑(totalWeight K) : ℝ) * log 2 + log (mulHeight₁ x) + log (mulHeight₁ y)

Tactic:
pull (disch := positivity) log

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ 0 < mulHeight₁ (x + y)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x + y)) ≤ log (HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ y)

Tactic:
exact (log_le_log <| by positivity) <| mulHeight₁_add_le ..

Premises used: Height.mulHeight₁_add_le, Real.log_le_log
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
rw : mulHeight₁ (x + -y) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ (-y)
⊢ mulHeight₁ (x - y) ≤ HPow.hPow (α := ℝ) 2 (totalWeight K) * mulHeight₁ x * mulHeight₁ y

Tactic:
rw [sub_eq_add_neg, ← mulHeight₁_neg y]

Premises used: sub_eq_add_neg, Height.mulHeight₁_neg
-- Module: Mathlib.NumberTheory.Height.Basic
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)

Tactic:
mulHeight₁_add_le x (-y)

Premises used: Height.mulHeight₁_add_le, Neg.neg
-- Module: Mathlib.NumberTheory.Height.Basic
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)

Tactic:
exact mulHeight₁_add_le x (-y)

Premises used: Height.mulHeight₁_add_le, Neg.neg
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
rw : logHeight₁ (x + -y) ≤ (↑(totalWeight K) : ℝ) * log 2 + logHeight₁ x + logHeight₁ (-y)
⊢ logHeight₁ (x - y) ≤ (↑(totalWeight K) : ℝ) * log 2 + logHeight₁ x + logHeight₁ y

Tactic:
rw [sub_eq_add_neg, ← logHeight₁_neg y]

Premises used: Height.logHeight₁_neg, sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Height.Basic
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)

Tactic:
logHeight₁_add_le x (-y)

Premises used: Height.logHeight₁_add_le, Neg.neg
-- Module: Mathlib.NumberTheory.Height.Basic
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)

Tactic:
exact logHeight₁_add_le x (-y)

Premises used: Height.logHeight₁_add_le, Neg.neg
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
f : Fin 2 → ℝ
rw : iSup ![f 0, f 1] = max (![f 0, f 1] 0) (![f 0, f 1] 1)
⊢ iSup f = max (f 0) (f 1)

Tactic:
rw [show f = ![f 0, f 1] from List.ofFn_inj.mp rfl]

Premises used: List.ofFn_inj, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
f : Fin 2 → ℝ
⊢ iSup ![f 0, f 1] = max (![f 0, f 1] 0) (![f 0, f 1] 1)

Tactic:
(max_eq_iSup ..).symm

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, _private.Mathlib.NumberTheory.Height.Basic.0.Height.max_eq_iSup, Fin.induction, Fin.cases, Eq.symm, Matrix.vecCons
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
f : Fin 2 → ℝ
⊢ iSup ![f 0, f 1] = max (![f 0, f 1] 0) (![f 0, f 1] 1)

Tactic:
exact (max_eq_iSup ..).symm

Premises used: _private.Mathlib.NumberTheory.Height.Basic.0.Height.max_eq_iSup, Eq.symm
-- 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 : β) → ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (∑ i ∈ ∅, l i) : ℝ) (⨆ (i : ↥∅), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)

Tactic:
simp
-- 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 : α)) : ℝ)
insert :
  LE.le (α := ℝ) ((v : (a : β) → ℝ) (l a + ∑ x ∈ s, l x) : ℝ)
    (⨆ (i : ↥(Insert.insert a 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 : α)) : ℝ)

Tactic:
rw [Finset.sum_insert ha]

Premises used: Finset.sum_insert
-- 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 : α)) : ℝ)
insert :
  LE.le (α := ℝ) (max ((v : (a : β) → ℝ) (l a)) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) : ℝ)
    (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : β) → ℝ) (l a + ∑ x ∈ s, l x) : ℝ)
    (⨆ (i : ↥(Insert.insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)

Tactic:
grw [hv .., ih]
-- 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 : α)) : ℝ)
⊢ LE.le (α := ℝ) (max ((v : (a : β) → ℝ) (l a)) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) : ℝ)
    (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)

Tactic:
max_le ?_ ?_

Premises used: max_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 : β) → ℝ)
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 : α)) : ℝ)
insert₁ :
  LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α)))
    (⨆ (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 : α)) : ℝ)

Tactic:
refine max_le ?_ ?_

Premises used: max_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 : β) → ℝ)
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) : ℝ) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)

Tactic:
Finite.le_ciSup_of_le ⟨_, s.mem_insert_self a⟩ le_rfl

Premises used: le_rfl, Finset.mem_insert_self, Subtype.mk, Finite.le_ciSup_of_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 : β) → ℝ)
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) : ℝ) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le ⟨_, s.mem_insert_self a⟩ le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_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 : β) → ℝ)
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 : α)))
insert₁ :
  ∀ (hs : Nonempty.{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 : α)))

Tactic:
rcases isEmpty_or_nonempty s with hs | hs

Premises used: Membership.mem, isEmpty_or_nonempty, Subtype
-- 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 : IsEmpty.{u_2 + 1} ↥s
⊢ LE.le (α := ℝ) (⨆ (i : ↥s), (v : (a : β) → ℝ) (l (↑i : α))) (⨆ (i : ↥(insert a s)), (v : (a : β) → ℝ) (l (↑i : α)))

Tactic:
simpa using Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Real.iSup_nonneg_of_nonnegHomClass
-- 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:
ciSup_le fun i ↦ Finite.le_ciSup_of_le (⟨i.val, Finset.mem_insert_of_mem i.prop⟩) le_rfl

Premises used: le_rfl, Subtype.mk, Finset.mem_insert_of_mem, Finite.le_ciSup_of_le, Subtype.prop, Subtype.val, ciSup_le