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
inst_2 : Finite ι
x y : ι → K
inl : ∀ (hι : IsEmpty ι), mulHeight (x * y) ≤ mulHeight x * mulHeight y
inr : ∀ (hι : Nonempty ι), mulHeight (x * y) ≤ mulHeight x * mulHeight y
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : IsEmpty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
inr : mulHeight (0 * y) ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 * mulHeight y
inr₁ : ∀ (hx : x ≠ 0), mulHeight (x * y) ≤ mulHeight x * mulHeight y
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
y : ι → K
hι : Nonempty ι
⊢ mulHeight (0 * y) ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 * mulHeight y

Tactic:
simpa using one_le_mulHeight y

Premises used: Height.one_le_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
inr : mulHeight (x * 0) ≤ mulHeight x * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
inr₁ : ∀ (hy : y ≠ 0), mulHeight (x * y) ≤ mulHeight x * mulHeight y
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
hι : Nonempty ι
hx : x ≠ 0
⊢ mulHeight (x * 0) ≤ mulHeight x * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0

Tactic:
simpa using one_le_mulHeight x

Premises used: Height.one_le_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
h : ∀ (x_1 : ι), (x * y) x_1 = ((fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)) x_1
⊢ x * y = (fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)

Tactic:
ext1
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
x_1 : ι
⊢ (x * y) x_1 = ((fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)) x_1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
inr :
  mulHeight.{u_1, u_2} (K := K) (ι := ι) ((fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)) ≤
    mulHeight.{u_1, u_2} (K := K) fun (a : ι × ι) ↦ x a.1 * y a.2
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
rw [← mulHeight_fun_mul_eq hx hy,
    show x * y = (fun a ↦ x a.1 * y a.2) ∘ fun i ↦ (i, i) by ext1; simp]

Premises used: Height.mulHeight_fun_mul_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) ((fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)) ≤
    mulHeight.{u_1, u_2} (K := K) fun (a : ι × ι) ↦ x a.1 * y a.2

Tactic:
mulHeight_comp_le ..

Premises used: Height.mulHeight_comp_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) ((fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)) ≤
    mulHeight.{u_1, u_2} (K := K) fun (a : ι × ι) ↦ x a.1 * y a.2

Tactic:
exact mulHeight_comp_le ..

Premises used: Height.mulHeight_comp_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
pull : log (mulHeight (x * y)) ≤ log (mulHeight x * mulHeight y)
⊢ log (mulHeight (x * y)) ≤ 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
ι : Type u_2
inst_2 : Finite ι
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
ι : Type u_2
inst_2 : Finite ι
x y : ι → K
⊢ log (mulHeight (x * y)) ≤ log (mulHeight x * mulHeight y)

Tactic:
exact log_le_log (by positivity) <| mulHeight_mul_le ..

Premises used: Height.mulHeight_mul_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
simp : mulHeight ![x * y, 1] ≤ mulHeight ![x, 1] * mulHeight ![y, 1]
⊢ mulHeight₁ (x * y) ≤ mulHeight₁ x * mulHeight₁ y

Tactic:
simp only [mulHeight₁_eq_mulHeight]

Premises used: Height.mulHeight₁_eq_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
h : ∀ (i : Fin (Nat.succ 0).succ), ![x * y, 1] i = (![x, 1] * ![y, 1]) i
⊢ ![x * y, 1] = ![x, 1] * ![y, 1]

Tactic:
ext i
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
i : Fin (Nat.succ 0).succ
h :
  ![x * y, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] * ![y, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![x * y, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] * ![y, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![x * y, 1] i = (![x, 1] * ![y, 1]) i

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] * ![y, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] * ![y, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
rw : mulHeight (![x, 1] * ![y, 1]) ≤ mulHeight ![x, 1] * mulHeight ![y, 1]
⊢ mulHeight ![x * y, 1] ≤ mulHeight ![x, 1] * mulHeight ![y, 1]

Tactic:
rw [show ![x * y, 1] = ![x, 1] * ![y, 1] by ext i; fin_cases i <;> simp]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ mulHeight (![x, 1] * ![y, 1]) ≤ mulHeight ![x, 1] * mulHeight ![y, 1]

Tactic:
mulHeight_mul_le ![x, 1] ![y, 1]

Premises used: Height.mulHeight_mul_le, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ mulHeight (![x, 1] * ![y, 1]) ≤ mulHeight ![x, 1] * mulHeight ![y, 1]

Tactic:
exact mulHeight_mul_le ![x, 1] ![y, 1]

Premises used: Height.mulHeight_mul_le, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- 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 (mulHeight₁ x * mulHeight₁ y)
⊢ log (mulHeight₁ (x * y)) ≤ 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 (mulHeight₁ x * mulHeight₁ y)

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

Premises used: Real.log_le_log, Height.mulHeight₁_mul_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ ∅, x i) ≤ ∏ i ∈ ∅, mulHeight₁ (x i)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
b : ι
s : Finset ι
hb : b ∉ s
ih : mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
insert : mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * ∏ i ∈ s, mulHeight₁ (x i)
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ Insert.insert b s, x i) ≤ ∏ i ∈ Insert.insert b s, mulHeight₁ (x i)

Tactic:
simp only [Finset.prod_insert hb]

Premises used: Finset.prod_insert
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
b : ι
s : Finset ι
hb : b ∉ s
ih : mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
insert : mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)
⊢ mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * ∏ i ∈ s, mulHeight₁ (x i)

Tactic:
grw [← ih]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
b : ι
s : Finset ι
hb : b ∉ s
ih : mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
⊢ mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)

Tactic:
mulHeight₁_mul_le ..

Premises used: Height.mulHeight₁_mul_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
b : ι
s : Finset ι
hb : b ∉ s
ih : mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
⊢ mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)

Tactic:
exact mulHeight₁_mul_le ..

Premises used: Height.mulHeight₁_mul_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
empty : mulHeight₁.{u_1} (K := K) (∏ i ∈ ∅, x i) ≤ ∏ i ∈ ∅, mulHeight₁ (x i)
insert :
  ∀ (b : ι) (s : Finset ι) (hb : b ∉ s) (ih : mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)),
    mulHeight₁.{u_1} (K := K) (∏ i ∈ Insert.insert b s, x i) ≤ ∏ i ∈ Insert.insert b s, mulHeight₁ (x i)
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert b s hb ih =>
    simp only [Finset.prod_insert hb]
    grw [← ih]
    exact mulHeight₁_mul_le ..

Premises used: Insert.insert, Height.mulHeight₁_mul_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
empty : mulHeight₁.{u_1} (K := K) (∏ i ∈ ∅, x i) ≤ ∏ i ∈ ∅, mulHeight₁ (x i)
insert :
  ∀ (b : ι) (s : Finset ι) (hb : b ∉ s) (ih : mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)),
    mulHeight₁.{u_1} (K := K) (∏ i ∈ Insert.insert b s, x i) ≤ ∏ i ∈ Insert.insert b s, mulHeight₁ (x i)
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert b s hb ih =>
    simp only [Finset.prod_insert hb]
    grw [← ih]
    exact mulHeight₁_mul_le ..

Premises used: Insert.insert, Height.mulHeight₁_mul_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
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
rw : log (mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)) ≤ log (∏ i ∈ s, mulHeight₁ (x i))
⊢ log (mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)) ≤ ∑ x_1 ∈ s, log (mulHeight₁ (x x_1))

Tactic:
rw [← log_prod (fun _ _ ↦ by positivity)]

Premises used: Real.log_prod
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
⊢ 0 < mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)

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
⊢ log (mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)) ≤ log (∏ i ∈ s, mulHeight₁ (x i))

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

Premises used: Height.mulHeight₁_prod_le, Real.log_le_log
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ max ((v : (a : R) → S) (∑ i ∈ s, x i)) 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
sup_le ?_ ?_

Premises used: sup_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
refine_1 : (v : (a : R) → S) (∑ i ∈ s, x i) ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
refine_2 : 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
⊢ max ((v : (a : R) → S) (∑ i ∈ s, x i)) 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
refine sup_le ?_ ?_

Premises used: sup_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
refine_1 :
  LE.le.{u_2} (α := S) ((v : (a : R) → S) (∑ i ∈ s, x i) : S) (∑ _x ∈ s, ∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)
⊢ (v : (a : R) → S) (∑ i ∈ s, x i) ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
rw [← nsmul_eq_mul, ← sum_const]

Premises used: nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
refine_1 : LE.le.{u_2} (α := S) (∑ i ∈ s, (v : (a : R) → S) (x i)) (∑ _x ∈ s, ∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) (∑ i ∈ s, x i) : S) (∑ _x ∈ s, ∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)

Tactic:
grw [v.sum_le s x]

Premises used: AbsoluteValue.sum_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
refine_1 :
  ∀ (i : ι) (hi : i ∈ s),
    LE.le.{u_2} (α := S) ((v : (a : R) → S) (x i) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)
⊢ LE.le.{u_2} (α := S) (∑ i ∈ s, (v : (a : R) → S) (x i)) (∑ _x ∈ s, ∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
gcongr with i hi
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
i : ι
hi : i ∈ s
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) (x i) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)

Tactic:
le_prod_max_one hi fun i ↦ v (x i)

Premises used: Finset.le_prod_max_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
i : ι
hi : i ∈ s
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) (x i) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)

Tactic:
exact le_prod_max_one hi fun i ↦ v (x i)

Premises used: Finset.le_prod_max_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
refine_2 : HMul.hMul (α := S) 1 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
⊢ 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
nth_rewrite 1 [← mul_one 1]

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
refine_2 : LE.le.{u_2} (α := S) 1 (↑(#s) : S)
refine_2₁ : LE.le.{u_2} (α := S) 1 (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
⊢ HMul.hMul (α := S) 1 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ LE.le.{u_2} (α := S) 1 (↑(#s) : S)

Tactic:
simp [hs]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ LE.le.{u_2} (α := S) 1 (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
s.one_le_prod fun _ _ ↦ le_max_right ..

Premises used: le_max_right, Finset.one_le_prod, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : LinearOrder S
inst_3 : IsOrderedRing S
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ LE.le.{u_2} (α := S) 1 (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
exact s.one_le_prod fun _ _ ↦ le_max_right ..

Premises used: le_max_right, Finset.one_le_prod, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.Basic
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
inl : LE.le.{u_2} (α := S) (max ((v : (a : R) → S) (∑ i ∈ ∅, x i)) 1 : S) (∏ i ∈ ∅, max ((v : (a : R) → S) (x i)) 1 : S)
inr :
  ∀ (hs : s.Nonempty),
    LE.le.{u_2} (α := S) (max ((v : (a : R) → S) (∑ i ∈ s, x i)) 1 : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)
⊢ LE.le.{u_2} (α := S) (max ((v : (a : R) → S) (∑ i ∈ s, x i)) 1 : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.NumberTheory.Height.Basic
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
x : ι → R
⊢ LE.le.{u_2} (α := S) (max ((v : (a : R) → S) (∑ i ∈ ∅, x i)) 1 : S) (∏ i ∈ ∅, max ((v : (a : R) → S) (x i)) 1 : S)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
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) (max ((v : (a : R) → S) (∑ i ∈ s, x i)) 1 : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)

Tactic:
sup_le ?_ <| s.one_le_prod fun _ _ ↦ le_max_right ..

Premises used: le_max_right, Finset.one_le_prod, sup_le, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.Basic
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
inr : 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)
⊢ LE.le.{u_2} (α := S) (max ((v : (a : R) → S) (∑ i ∈ s, x i)) 1 : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)

Tactic:
refine sup_le ?_ <| s.one_le_prod fun _ _ ↦ le_max_right ..

Premises used: le_max_right, Finset.one_le_prod, sup_le, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.Basic
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
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)
⊢ 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)

Tactic:
grw [hv.apply_sum_le_sup hs]

Premises used: IsNonarchimedean.apply_sum_le_sup
-- Module: Mathlib.NumberTheory.Height.Basic
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) (s.sup' hs fun (i : ι) ↦ (v : (a : R) → S) (x i)) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
sup'_le hs (fun i ↦ v (x i)) fun i hi ↦ le_prod_max_one hi fun i ↦ v (x i)

Premises used: Finset.le_prod_max_one, Finset.sup'_le, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.Basic
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) (s.sup' hs fun (i : ι) ↦ (v : (a : R) → S) (x i)) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)

Tactic:
exact sup'_le hs (fun i ↦ v (x i)) fun i hi ↦ le_prod_max_one hi fun i ↦ v (x i)

Premises used: Finset.le_prod_max_one, Finset.sup'_le, DFunLike.coe
-- 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
⊢ ∀ b ∈ s,
    Function.HasFiniteMulSupport (M := ℝ) fun (a : (↑nonarchAbsVal : Type u_1)) ↦
      max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x b)) 1

Tactic:
fun_prop