awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
⊢ (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = mulHeight x * mulHeight y
have rw : HMul.hMul (α := ℝ)
    (Multiset.prod
      (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι × ι'), (v : (a : K) → ℝ) (x i.1 * y i.2)) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι × ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i.1 * y i.2)) =
  HMul.hMul (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (i : AbsoluteValue K ℝ) ↦
          HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι'), (i : (a : K) → ℝ) (y i_1)))
        archAbsVal))
    (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)),
      HMul.hMul (α := ℝ) (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1))
        (⨆ (i_1 : ι'), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (y i_1)))
Tactic: rw [mulHeight_eq hx, mulHeight_eq hy, mulHeight_eq hxy, mul_mul_mul_comm, ← Multiset.prod_map_mul,
    ← finprod_mul_distrib
        (hasFiniteMulSupport_iSup_nonarchAbsVal hx) (hasFiniteMulSupport_iSup_nonarchAbsVal hy)]
-- 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι × ι'), (v : (a : K) → ℝ) (x i.1 * y i.2)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι × ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i.1 * y i.2)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (i : AbsoluteValue K ℝ) ↦
            HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι'), (i : (a : K) → ℝ) (y i_1)))
          archAbsVal))
      (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)),
        HMul.hMul (α := ℝ) (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1))
          (⨆ (i_1 : ι'), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (y i_1)))
have e_a : Eq.{u_1 + 1} (α := AbsoluteValue K ℝ → ℝ)
  (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι × ι'), (v : (a : K) → ℝ) (x i.1 * y i.2)) fun (i : AbsoluteValue K ℝ) ↦
  HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι'), (i : (a : K) → ℝ) (y i_1))
Tactic: congr
-- 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
e_a :
  Eq.{u_1 + 1} (α := AbsoluteValue K ℝ → ℝ)
    (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι × ι'), (v : (a : K) → ℝ) (x i.1 * y i.2)) fun (i : AbsoluteValue K ℝ) ↦
    HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι'), (i : (a : K) → ℝ) (y i_1))
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι × ι'), (v : (a : K) → ℝ) (x i.1 * y i.2)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι × ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i.1 * y i.2)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map
          (fun (i : AbsoluteValue K ℝ) ↦
            HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι'), (i : (a : K) → ℝ) (y i_1)))
          archAbsVal))
      (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)),
        HMul.hMul (α := ℝ) (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1))
          (⨆ (i_1 : ι'), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (y i_1)))
have e_a₁ : Eq.{u_1 + 1} (α := (↑nonarchAbsVal : Type u_1) → ℝ)
  (fun (v : (↑nonarchAbsVal : Type u_1)) ↦ ⨆ (i : ι × ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i.1 * y i.2))
  fun (i : (↑nonarchAbsVal : Type u_1)) ↦
  HMul.hMul (α := ℝ) (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1))
    (⨆ (i_1 : ι'), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (y i_1))
Tactic: congr
-- 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
⊢ Eq.{u_1 + 1} (α := AbsoluteValue K ℝ → ℝ)
    (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι × ι'), (v : (a : K) → ℝ) (x i.1 * y i.2)) fun (i : AbsoluteValue K ℝ) ↦
    HMul.hMul (α := ℝ) (⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) (⨆ (i_1 : ι'), (i : (a : K) → ℝ) (y i_1))
have e_a : ∀ (v : AbsoluteValue K ℝ),
  ⨆ (i : ι × ι'), (v : (a : K) → ℝ) (x i.1 * y i.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (y i))
Tactic: ext1 v
-- 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
⊢ Eq.{u_1 + 1} (α := (↑nonarchAbsVal : Type u_1) → ℝ)
    (fun (v : (↑nonarchAbsVal : Type u_1)) ↦ ⨆ (i : ι × ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i.1 * y i.2))
    fun (i : (↑nonarchAbsVal : Type u_1)) ↦
    HMul.hMul (α := ℝ) (⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1))
      (⨆ (i_1 : ι'), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (y i_1))
have e_a : ∀ (v : (↑nonarchAbsVal : Type u_1)),
  ⨆ (i : ι × ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i.1 * y i.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
      (⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (y i))
Tactic: ext1 v
-- 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
⊢ log (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = log (mulHeight x) + log (mulHeight y)
have pull : log (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = log (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
ι : Type u_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
⊢ log (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = log (mulHeight x * mulHeight y)
have rw : log (mulHeight x * mulHeight y) = log (mulHeight x * mulHeight y)
Tactic: rw [mulHeight_fun_mul_eq hx hy]
-- 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
x : ι → K
⊢ mulHeight (-x) = mulHeight x
have inl : mulHeight.{u_1, u_2} (K := K) (ι := ι) (-0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- 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
x : ι → K
inl : mulHeight.{u_1, u_2} (K := K) (ι := ι) (-0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
⊢ mulHeight (-x) = mulHeight x
have inr : ∀ (hx : x ≠ 0), mulHeight (-x) = mulHeight x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- 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
inst_2 : Finite ι
x y : ι → K
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
have inl : ∀ (hι : IsEmpty ι), mulHeight (x * y) ≤ mulHeight x * mulHeight y
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- 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
inst_2 : Finite ι
x y : ι → K
inl : ∀ (hι : IsEmpty ι), mulHeight (x * y) ≤ mulHeight x * mulHeight y
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
have inr : ∀ (hι : Nonempty ι), mulHeight (x * y) ≤ mulHeight x * mulHeight y
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- 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
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
have inr : mulHeight (0 * y) ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 * mulHeight y
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- 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
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
inr : mulHeight (0 * y) ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 * mulHeight y
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
have inr₁ : ∀ (hx : x ≠ 0), mulHeight (x * y) ≤ mulHeight x * mulHeight y
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- 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
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
have inr : mulHeight (x * 0) ≤ mulHeight x * mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y
-- 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
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
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
have inr₁ : ∀ (hy : y ≠ 0), mulHeight (x * y) ≤ mulHeight x * mulHeight y
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- 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
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = (fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)
have h : ∀ (x_1 : ι), (x * y) x_1 = ((fun (a : ι × ι) ↦ x a.1 * y a.2) ∘ fun (i : ι) ↦ (i, i)) x_1
Tactic: ext1
-- 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
inst_2 : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
have 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
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]
-- 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
inst_2 : Finite ι
x y : ι → K
⊢ log (mulHeight (x * y)) ≤ log (mulHeight x) + log (mulHeight y)
have pull : log (mulHeight (x * y)) ≤ log (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) ≤ mulHeight₁ x * mulHeight₁ y
have simp : mulHeight ![x * y, 1] ≤ mulHeight ![x, 1] * mulHeight ![y, 1]
Tactic: simp only [mulHeight₁_eq_mulHeight]
-- 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
⊢ ![x * y, 1] = ![x, 1] * ![y, 1]
have h : ∀ (i : Fin (Nat.succ 0).succ), ![x * y, 1] i = (![x, 1] * ![y, 1]) i
Tactic: ext i
-- 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
i : Fin (Nat.succ 0).succ
⊢ ![x * y, 1] i = (![x, 1] * ![y, 1]) i
have h : ![x * y, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
  (![x, 1] * ![y, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
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, ⋯⟩)
⊢ ![x * y, 1] i = (![x, 1] * ![y, 1]) i
have h₁ : ![x * y, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
  (![x, 1] * ![y, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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, 1] ≤ mulHeight ![x, 1] * mulHeight ![y, 1]
have rw : mulHeight (![x, 1] * ![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]
-- 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)) ≤ log (mulHeight₁ x) + log (mulHeight₁ y)
have pull : log (mulHeight₁ (x * y)) ≤ log (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
ι : 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₁.{u_1} (K := K) (∏ i ∈ insert b s, x i) ≤ ∏ i ∈ insert b s, mulHeight₁ (x i)
have insert : mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * ∏ i ∈ s, mulHeight₁ (x i)
Tactic: simp only [Finset.prod_insert hb]
-- 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
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) * ∏ i ∈ s, mulHeight₁ (x i)
have insert : mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)
Tactic: grw [← ih]
-- 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
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
have empty : mulHeight₁.{u_1} (K := K) (∏ i ∈ ∅, x i) ≤ ∏ i ∈ ∅, 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 ..
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
empty : mulHeight₁.{u_1} (K := K) (∏ i ∈ ∅, x i) ≤ ∏ i ∈ ∅, mulHeight₁ (x i)
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
have 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 b s, x i) ≤ ∏ i ∈ insert b 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 ..
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
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
have empty : mulHeight₁.{u_1} (K := K) (∏ i ∈ ∅, x i) ≤ ∏ i ∈ ∅, 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 ..
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
empty : mulHeight₁.{u_1} (K := K) (∏ i ∈ ∅, x i) ≤ ∏ i ∈ ∅, mulHeight₁ (x i)
⊢ mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
have 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 b s, x i) ≤ ∏ i ∈ insert b 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 ..
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
⊢ log (mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)) ≤ ∑ x_1 ∈ s, log (mulHeight₁ (x x_1))
have rw : log (mulHeight₁.{u_1} (K := K) (∏ i ∈ s, x i)) ≤ log (∏ i ∈ s, mulHeight₁ (x i))
Tactic: rw [← log_prod (fun _ _ ↦ by positivity)]
-- 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
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)
have 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)
Tactic: refine sup_le ?_ ?_
-- 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
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)
⊢ 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)
have refine_2 : 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
Tactic: refine sup_le ?_ ?_
-- 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
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ (v : (a : R) → S) (∑ i ∈ s, x i) ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
have 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)
Tactic: rw [← nsmul_eq_mul, ← sum_const]
-- 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
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 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)
have 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)
Tactic: grw [v.sum_le s x]
-- 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
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 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)
have 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)
Tactic: gcongr with i hi
-- 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
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
have refine_2 : HMul.hMul (α := S) 1 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
Tactic: nth_rewrite 1 [← mul_one 1]
-- 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
inst_4 : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ HMul.hMul (α := S) 1 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
have refine_2 : LE.le.{u_2} (α := S) 1 (↑(#s) : S)
Tactic: gcongr
-- 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
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)
⊢ HMul.hMul (α := S) 1 1 ≤ HMul.hMul (α := S) (↑(#s) : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
have refine_2₁ : LE.le.{u_2} (α := S) 1 (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1)
Tactic: gcongr
-- 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
⊢ 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)
have 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)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s
-- 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
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)
⊢ 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)
have 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)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- 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) (max ((v : (a : R) → S) (∑ i ∈ s, x i)) 1 : S) (∏ i ∈ s, max ((v : (a : R) → S) (x i)) 1 : S)
have 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)
Tactic: refine sup_le ?_ <| s.one_le_prod fun _ _ ↦ le_max_right ..