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
hι : IsEmpty ι
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 = 1

Tactic:
exact mulHeight_zero

Premises used: Height.mulHeight_zero
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
hι : Nonempty ι
⊢ Ne (α := ι → K) 1 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
hι : Nonempty ι
⊢ Ne (α := ι → K) 1 0

Tactic:
have hx : (1 : ι → K) ≠ 0 := by simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
hι : Nonempty ι
hx : Ne (α := ι → K) 1 0
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1

Tactic:
simp [mulHeight_eq hx]

Premises used: Height.mulHeight_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
⊢ ∀ (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)
-- Module: Mathlib.NumberTheory.Height.Basic
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
inr : ∀ (hx : x ≠ 0), mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = mulHeight x
⊢ mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = mulHeight x

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
ι' : Type u_3
e : ι ≃ ι'
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:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ ∃ (i : ι'), x i ≠ 0

Tactic:
ne_iff.mp hx

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Height.Basic
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
obtain : ∀ (i : ι') (hi : x i ≠ 0), Ne (α := ι → K) (x ∘ (⇑e : (a : ι) → ι')) 0
⊢ Ne (α := ι → K) (x ∘ (⇑e : (a : ι) → ι')) 0

Tactic:
obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := ne_iff.mp hx

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Height.Basic
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
i : ι'
hi : x i ≠ 0
⊢ comp.{u_2 + 1, u_3 + 1, u_1 + 1} (α := ι) x ((⇑e : (a : ι) → ι') : (a : ι) → ι') ((e.symm : (a : ι') → ι) i : ι) ≠
    0 ((e.symm : (a : ι') → ι) i)

Tactic:
simp [hi]
-- Module: Mathlib.NumberTheory.Height.Basic
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
i : ι'
hi : x i ≠ 0
⊢ Ne (α := ι → K) (x ∘ (⇑e : (a : ι) → ι')) 0

Tactic:
exact ne_iff.mpr ⟨e.symm i, by simp [hi]⟩

Premises used: Iff.mpr, Function.ne_iff, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.Basic
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

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]⟩
-- Module: Mathlib.NumberTheory.Height.Basic
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
hx' : Ne (α := ι → K) (x ∘ (⇑e : (a : ι) → ι')) 0
⊢ mulHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = mulHeight x

Tactic:
simp [mulHeight_eq hx, mulHeight_eq hx', comp_apply, H]

Premises used: Height.mulHeight_eq, Function.comp_apply
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
rw : mulHeight (ι := Fin (Nat.succ 0).succ) (![y, x] ∘ (⇑e : (a : Fin 2) → Fin 2)) = mulHeight ![y, x]
⊢ mulHeight ![x, y] = mulHeight ![y, x]

Tactic:
rw [show ![x, y] = ![y, x] ∘ e from List.ofFn_inj.mp rfl]

Premises used: List.ofFn_inj, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
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 (ι := Fin (Nat.succ 0).succ) (![y, x] ∘ (⇑e : (a : Fin 2) → Fin 2)) = mulHeight ![y, x]

Tactic:
mulHeight_comp_equiv e ![y, x]

Premises used: Height.mulHeight_comp_equiv, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.NumberTheory.Height.Basic
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 (ι := Fin (Nat.succ 0).succ) (![y, x] ∘ (⇑e : (a : Fin 2) → Fin 2)) = mulHeight ![y, x]

Tactic:
exact mulHeight_comp_equiv e ![y, x]

Premises used: Height.mulHeight_comp_equiv, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
⊢ logHeight x = log (mulHeight x)

Tactic:
rfl

Premises used: Height.logHeight, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
⊢ logHeight.{u_1, u_2} (K := K) (ι := ι) 0 = 0

Tactic:
simp [logHeight_eq_log_mulHeight]

Premises used: Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
⊢ logHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 0

Tactic:
simp [logHeight_eq_log_mulHeight]

Premises used: Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
⊢ logHeight.{u_1, u_2} (ι := ι) (x ∘ (⇑e : (a : ι) → ι')) = logHeight x

Tactic:
simp only [logHeight_eq_log_mulHeight, mulHeight_comp_equiv]

Premises used: Height.mulHeight_comp_equiv, Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
⊢ logHeight ![x, y] = logHeight ![y, x]

Tactic:
simp only [logHeight_eq_log_mulHeight, mulHeight_swap]

Premises used: Height.mulHeight_swap, Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u_4
x : α →₀ K
⊢ logHeight.{u_1, u_4} (K := K) (ι := α) (⇑x : (a : α) → K) =
    log (mulHeight.{u_1, u_4} (K := K) (ι := α) (⇑x : (a : α) → K))

Tactic:
rfl

Premises used: Height.logHeight, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
α : Type u_5
inst : ConditionallyCompleteLattice α
a b : α
⊢ ∀ (c : α), a ⊔ b ≤ c ↔ iSup ![a, b] ≤ c

Tactic:
simp [ciSup_le_iff, Fin.forall_fin_two]

Premises used: Fin.forall_fin_two, ciSup_le_iff
-- 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
hx : x ≠ 0
⊢ Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }

Tactic:
have : Nonempty {j // x j ≠ 0} := nonempty_subtype.mpr <| ne_iff.mp hx
-- 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
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 : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))

Tactic:
this
-- 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
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 : ι))
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 : ι)))
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)

Tactic:
convert! this with v
-- 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
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)
⊢ ∃ (j : ι), x j ≠ 0

Tactic:
Function.ne_iff.mp hx

Premises used: Function.ne_iff, Iff.mp
-- 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
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)
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 : ι)))
⊢ 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

Premises used: Function.ne_iff, Iff.mp
-- 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
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
⊢ Nonempty ι

Tactic:
have : Nonempty ι := .intro i
-- 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
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 : ι)))

Tactic:
le_antisymm (ciSup_le fun j ↦ ?_) (ciSup_le fun ⟨j, hj⟩ ↦ Finite.le_ciSup_of_le j le_rfl)

Premises used: le_rfl, iSup, _private.0.Height.hasFiniteMulSupport_iSup_nonarchAbsVal.match_1, LE.le, le_antisymm, Finite.le_ciSup_of_le, Subtype.val, DFunLike.coe, ciSup_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 : ι → 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 ι
h :
  ∀ (j : ι),
    LE.le (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x j) : ℝ)
      (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)) : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
    (⨆ (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)

Premises used: le_antisymm, ciSup_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 : ι → 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 : ι)) : ℝ)
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 : ι)) : ℝ)

Tactic:
rcases eq_or_ne (x j) 0 with h | h

Premises used: eq_or_ne, OfNat.ofNat
-- 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
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
h₁ : LE.le (α := ℝ) 0 (⨆ (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 : ι)) : ℝ)

Tactic:
rw [h, v.val.map_zero]

Premises used: Subtype.val, AbsoluteValue.map_zero
-- 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
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 (α := ℝ) 0 (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))

Tactic:
Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩

Premises used: Real.iSup_nonneg', AbsoluteValue.nonneg, Subtype.mk, Exists.intro, Subtype.val
-- 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
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 (α := ℝ) 0 (⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι)))

Tactic:
exact Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩

Premises used: Real.iSup_nonneg', AbsoluteValue.nonneg, Exists.intro, Subtype.val
-- 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
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 : ι)) : ℝ)

Tactic:
Finite.le_ciSup_of_le ⟨j, h⟩ le_rfl

Premises used: le_rfl, Subtype.mk, Finite.le_ciSup_of_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 : ι → 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 : ι)) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le ⟨j, h⟩ le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_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 : ι → K
hx : x ≠ 0
this : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
suffices :
  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)

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
-- 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
hx : x ≠ 0
this : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
i : { j : ι // x j ≠ 0 }
⊢ x (↑i : ι) ≠ 0

Tactic:
grind
-- 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
hx : x ≠ 0
this : Nonempty.{max 1 (u_2 + 1)} { j : ι // x j ≠ 0 }
funProp : ∀ (i : { j : ι // x j ≠ 0 }), x (↑i : ι) ≠ 0
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : { j : ι // x j ≠ 0 }), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x (↑i : ι))

Tactic:
fun_prop (disch := grind)
-- Module: Mathlib.NumberTheory.Height.Basic
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
inr :
  ∀ (hx : x ≠ 0),
    HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
      max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1
⊢ 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

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
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) 0) 1

Tactic:
simp [HasFiniteMulSupport]

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx funProp : x ≠ 0
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1

Tactic:
fun_prop
-- 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
c : K
hc : c ≠ 0
inl : mulHeight (HSMul.hSMul (β := ι → K) c 0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
inr : ∀ (hx : x ≠ 0), mulHeight (c • x) = mulHeight x
⊢ mulHeight (c • x) = mulHeight x

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 ι
c : K
hc : c ≠ 0
inl inl₁ : mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
⊢ mulHeight (HSMul.hSMul (β := ι → K) c 0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- 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
c : K
hc : c ≠ 0
hx : x ≠ 0
⊢ Nonempty ι

Tactic:
have : Nonempty ι := (ne_iff.mp hx).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 : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ c • x ≠ 0

Tactic:
simp [hc, hx]
-- 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
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ c • x ≠ 0

Tactic:
have hcx : c • x ≠ 0 := by simp [hc, hx]