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
x : K
H :
  HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1) ≠
    0
this :
  ∀ (a : ℝ),
    Membership.mem (γ := Multiset ℝ)
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal) a →
      a ≠ 0
⊢ log
      (HMul.hMul (α := ℝ)
        (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1)) =
    HAdd.hAdd (α := ℝ)
      (Multiset.sum (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal))
      (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x))
have rw : HAdd.hAdd (α := ℝ)
    (Multiset.sum
      (Multiset.map.{0, u_1} (α := AbsoluteValue K ℝ)
        ((fun (x : ℝ) ↦ log x) ∘ fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
    (∑ᶠ (a : (↑nonarchAbsVal : Type u_1)), log (max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1)) =
  HAdd.hAdd (α := ℝ) (Multiset.sum (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal))
    (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x))
Tactic: rw [log_mul (left_ne_zero_of_mul H) (right_ne_zero_of_mul H), log_multiset_prod this,
    Multiset.map_map, log_finprod (fun _ ↦ by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1) ≠
    0
this :
  ∀ (a : ℝ),
    Membership.mem (γ := Multiset ℝ)
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal) a →
      a ≠ 0
⊢ HAdd.hAdd (α := ℝ)
      (Multiset.sum
        (Multiset.map.{0, u_1} (α := AbsoluteValue K ℝ)
          ((fun (x : ℝ) ↦ log x) ∘ fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∑ᶠ (a : (↑nonarchAbsVal : Type u_1)), log (max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1)) =
    HAdd.hAdd (α := ℝ)
      (Multiset.sum (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal))
      (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x))
have e_a : Eq (α := Multiset ℝ)
  (Multiset.map.{0, u_1} (α := AbsoluteValue K ℝ)
    ((fun (x : ℝ) ↦ log x) ∘ fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal)
  (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1) ≠
    0
this :
  ∀ (a : ℝ),
    Membership.mem (γ := Multiset ℝ)
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal) a →
      a ≠ 0
e_a :
  Eq (α := Multiset ℝ)
    (Multiset.map.{0, u_1} (α := AbsoluteValue K ℝ)
      ((fun (x : ℝ) ↦ log x) ∘ fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal)
    (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal)
⊢ HAdd.hAdd (α := ℝ)
      (Multiset.sum
        (Multiset.map.{0, u_1} (α := AbsoluteValue K ℝ)
          ((fun (x : ℝ) ↦ log x) ∘ fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∑ᶠ (a : (↑nonarchAbsVal : Type u_1)), log (max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1)) =
    HAdd.hAdd (α := ℝ)
      (Multiset.sum (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal))
      (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x))
have e_a₁ : Eq.{u_1 + 1} (α := (↑nonarchAbsVal : Type u_1) → ℝ)
  (fun (a : (↑nonarchAbsVal : Type u_1)) ↦ log (max (((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1))
  fun (v : (↑nonarchAbsVal : Type u_1)) ↦ log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x)
Tactic: congr 2
-- 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
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
have inl : ∀ (hι : IsEmpty ι), mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
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
inl : ∀ (hι : IsEmpty ι), mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
have inr : ∀ (hι : Nonempty ι), mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
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
hι : IsEmpty ι
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
have inl : mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 = 1
Tactic: rw [show (1 : ι → K) = 0 from Subsingleton.elim ..]
-- 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
hι : Nonempty ι
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
have hx : Ne (α := ι → K) 1 0
Tactic: have hx : (1 : ι → K) ≠ 0 := by simp
-- 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
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
⊢ mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = mulHeight x
have H : ∀ (v : AbsoluteValue K ℝ),
  Eq (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x ((e : (a : ι) → ι') i))) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
Tactic: have H (v : AbsoluteValue K ℝ) : ⨆ i, v (x (e i)) = ⨆ i, v (x i) := e.iSup_congr (congrFun rfl)
-- 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
e : ι ≃ ι'
x : ι' → K
H :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x ((e : (a : ι) → ι') i))) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = mulHeight x
have inl : ∀
  (H :
    ∀ (v : AbsoluteValue K ℝ),
      Eq (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (0 ((e : (a : ι) → ι') i))) (⨆ (i : ι'), (v : (a : K) → ℝ) (0 i))),
  mulHeight.{u_1, u_2} (K := K) (ι := ι) (comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := ι') 0 (⇑e : (a : ι) → ι')) =
    mulHeight.{u_1, u_3} (K := K) (ι := ι') 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x, 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
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
H :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x ((e : (a : ι) → ι') i))) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
inl :
  ∀
    (H :
      ∀ (v : AbsoluteValue K ℝ),
        Eq (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (0 ((e : (a : ι) → ι') i))) (⨆ (i : ι'), (v : (a : K) → ℝ) (0 i))),
    mulHeight.{u_1, u_2} (K := K) (ι := ι) (comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := ι') 0 (⇑e : (a : ι) → ι')) =
      mulHeight.{u_1, u_3} (K := K) (ι := ι') 0
⊢ mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = mulHeight x
have inr : ∀ (hx : x ≠ 0), mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = 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
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
H :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x ((e : (a : ι) → ι') i))) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
hx : x ≠ 0
⊢ Ne (α := ι → K) (x ∘ (⇑e : (a : ι) → ι')) 0
have obtain : ∀ (i : ι') (hi : x i ≠ 0), Ne (α := ι → K) (x ∘ (⇑e : (a : ι) → ι')) 0
Tactic: obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := ne_iff.mp hx
-- 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
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
H :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x ((e : (a : ι) → ι') i))) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
hx : x ≠ 0
⊢ mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = mulHeight x
have hx' : Ne (α := ι → K) (x ∘ (⇑e : (a : ι) → ι')) 0
Tactic: have hx' : x ∘ e ≠ 0 := by
      obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := ne_iff.mp hx
      exact ne_iff.mpr ⟨e.symm i, by simp [hi]⟩
-- 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
e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
⊢ mulHeight ![x, y] = mulHeight ![y, x]
have rw : mulHeight (ι := Fin (Nat.succ 0).succ) (![y, x] ∘ (⇑e : (a : Fin 2) → Fin 2)) = mulHeight ![y, x]
Tactic: rw [show ![x, y] = ![y, x] ∘ e from List.ofFn_inj.mp rfl]
-- 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
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
have this : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
Tactic: have : Nonempty {j // x j ≠ 0} := nonempty_subtype.mpr <| ne_iff.mp 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 : ι → K
hx : x ≠ 0
this_1 : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
this :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
have h : ∀ (v : (↑nonarchAbsVal : Type u_1)),
  Eq (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))
Tactic: convert! this with 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
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
this_1 : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
this :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
v : (↑nonarchAbsVal : Type u_1)
⊢ Eq (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))
have h : ∀ (i : ι) (hi : x i ≠ 0),
  Eq (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))
Tactic: obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
-- 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
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
this_1 : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
this :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
v : (↑nonarchAbsVal : Type u_1)
i : ι
hi : x i ≠ 0
⊢ Eq (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))
have this₁ : Nonempty ι
Tactic: have : Nonempty ι := .intro i
-- 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 : ι → K
hx : x ≠ 0
this_1 : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
this_2 :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
v : (↑nonarchAbsVal : Type u_1)
i : ι
hi : x i ≠ 0
this : Nonempty ι
⊢ Eq (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))
have h : ∀ (j : ι),
  LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
Tactic: refine le_antisymm (ciSup_le fun j ↦ ?_) (ciSup_le fun ⟨j, hj⟩ ↦ Finite.le_ciSup_of_le j le_rfl)
-- 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 : ι → K
hx : x ≠ 0
this_1 : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
this_2 :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
v : (↑nonarchAbsVal : Type u_1)
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
⊢ LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
have h : ∀ (h : x j = 0),
  LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
Tactic: rcases eq_or_ne (x j) 0 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 : ι → K
hx : x ≠ 0
this_1 : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
this_2 :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
v : (↑nonarchAbsVal : Type u_1)
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h :
  ∀ (h : x j = 0),
    LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
      (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
⊢ LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
have h₁ : ∀ (h : x j ≠ 0),
  LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
Tactic: rcases eq_or_ne (x j) 0 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 : ι → K
hx : x ≠ 0
this_1 : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
this_2 :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
v : (↑nonarchAbsVal : Type u_1)
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j = 0
⊢ LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
    (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
have h₁ : LE.le (α := ℝ) 0 (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))
Tactic: rw [h, v.val.map_zero]
-- 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 : ι → K
hx : x ≠ 0
this : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
have suffices : HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
  ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
Tactic: suffices (fun v : nonarchAbsVal ↦ ⨆ i : {j // x j ≠ 0}, v.val (x i)).HasFiniteMulSupport by
    convert! this with v
    obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
    have : Nonempty ι := .intro i
    refine le_antisymm (ciSup_le fun j ↦ ?_) (ciSup_le fun ⟨j, hj⟩ ↦ Finite.le_ciSup_of_le j le_rfl)
    rcases eq_or_ne (x j) 0 with h | h
    · rw [h, v.val.map_zero]
      exact Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩
    · exact Finite.le_ciSup_of_le ⟨j, h⟩ le_rfl
-- 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 : ι → K
hx : x ≠ 0
this : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))
have funProp : ∀ (i : { j : ι // x j ≠ 0 }), x (↑i : ι) ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1
have inl : HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦ max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) 0) 1
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
x : K
inl :
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) 0) 1
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1
have inr : ∀ (hx : x ≠ 0),
  HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1
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 : ι → K
c : K
hc : c ≠ 0
⊢ mulHeight (c • x) = mulHeight x
have inl : mulHeight (HSMul.hSMul (β := ι → K) c 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
inst_2 : Finite ι
x : ι → K
c : K
hc : c ≠ 0
inl : mulHeight (HSMul.hSMul (β := ι → K) c 0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
⊢ mulHeight (c • x) = mulHeight x
have inr : ∀ (hx : x ≠ 0), mulHeight (c • 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 ι
c : K
hc : c ≠ 0
⊢ mulHeight (HSMul.hSMul (β := ι → K) c 0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
have inl : mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
Tactic: rw [smul_zero]
-- 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
inst_2 : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
⊢ mulHeight (c • x) = mulHeight x
have this : Nonempty ι
Tactic: have : Nonempty ι := (ne_iff.mp hx).nonempty
-- 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
inst_2 : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ mulHeight (c • x) = mulHeight x
have hcx : c • x ≠ 0
Tactic: have hcx : c • x ≠ 0 := by simp [hc, 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 : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
⊢ mulHeight (c • x) = mulHeight x
have inr : HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal)) *
    ∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      HMul.hMul (α := ℝ) (β := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) c : ℝ)
        (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i) : ℝ) =
  HMul.hMul (α := ℝ)
    (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
Tactic: simp only [mulHeight_eq hx, mulHeight_eq hcx, Pi.smul_apply, smul_eq_mul, map_mul,
    ← mul_iSup_of_nonneg <| AbsoluteValue.nonneg .., Multiset.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
inst_2 : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
⊢ HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
        (Multiset.prod
          (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal)) *
      ∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        HMul.hMul (α := ℝ) (β := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) c : ℝ)
          (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i) : ℝ) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
have inr : HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal)) *
    HMul.hMul (α := ℝ) (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) c)
      (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
  HMul.hMul (α := ℝ)
    (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
Tactic: rw [finprod_mul_distrib (by fun_prop) (by fun_prop),
    mul_mul_mul_comm, product_formula hc, one_mul]