awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] ^ n) ((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 : K
n : ℕ
⊢ logHeight₁ (x ^ n) = (↑n : ℝ) * logHeight₁ x

Tactic:
simp only [logHeight₁_eq_log_mulHeight₁, mulHeight₁_pow, log_pow]

Premises used: Height.mulHeight₁_pow, Real.log_pow, Height.logHeight₁_eq_log_mulHeight₁
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
inl : ∀ (h : 0 ≤ n), mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
inr : ∀ (h : n < 0), mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

Tactic:
rcases le_or_gt 0 n with h | h

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : 0 ≤ n
⊢ 0 ≤ n

Tactic:
h
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : 0 ≤ n
inl : ∀ (n : ℕ), mulHeight₁ (HPow.hPow (β := ℤ) x (↑n : ℤ)) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

Tactic:
lift n to ℕ using h
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
inl : mulHeight₁ (x ^ n) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
inl₁ : mulHeight₁ x ^ n = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
inl₂ inl₃ : mulHeight₁ x ^ n = mulHeight₁ x ^ n
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (↑n : ℤ)) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)

Tactic:
rw [zpow_natCast, mulHeight₁_pow, Int.natAbs_natCast]

Premises used: zpow_natCast, Height.mulHeight₁_pow, Int.natAbs_natCast
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ n = -(↑n.natAbs : ℤ)

Tactic:
grind
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
inr : mulHeight₁ (HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ))) = mulHeight₁ x ^ n.natAbs
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

Tactic:
nth_rewrite 1 [show n = -n.natAbs by grind]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
inr : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ))⁻¹ = mulHeight₁ x ^ n.natAbs
inr₁ : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ)) = mulHeight₁ x ^ n.natAbs
inr₂ : mulHeight₁ (x ^ n.natAbs) = mulHeight₁ x ^ n.natAbs
inr₃ inr₄ : mulHeight₁ x ^ n.natAbs = mulHeight₁ x ^ n.natAbs
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ))) = mulHeight₁ x ^ n.natAbs

Tactic:
rw [zpow_neg, mulHeight₁_inv, zpow_natCast, mulHeight₁_pow]

Premises used: zpow_natCast, Height.mulHeight₁_pow, Height.mulHeight₁_inv, zpow_neg
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
⊢ logHeight₁ (x ^ n) = (↑n.natAbs : ℝ) * logHeight₁ x

Tactic:
simp only [logHeight₁_eq_log_mulHeight₁, mulHeight₁_zpow, log_pow]

Premises used: Height.mulHeight₁_zpow, Real.log_pow, Height.logHeight₁_eq_log_mulHeight₁
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
rw :
  HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : (a : α) → ι a), (v : (a : K) → ℝ) (∏ a : α, x a (i a)))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : (a : α) → ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∏ a : α, x a (i a))) =
    ∏ a : α, mulHeight (x a)
rw₁ : Ne (α := ((a : α) → ι a) → K) (fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) 0
⊢ (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = ∏ a : α, mulHeight (x a)

Tactic:
rw [mulHeight_eq ?h₁]

Premises used: Height.mulHeight_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
simp_rw :
  ∀ (hx : ∀ (a : α), ∃ (a_1 : ι a), x a a_1 ≠ 0),
    ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0
⊢ Ne (α := ((a : α) → ι a) → K) (fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) 0

Tactic:
simp_rw [ne_iff, Pi.zero_def] at hx ⊢

Premises used: Pi.zero_def, Function.ne_iff
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), ∃ (a_1 : ι a), x a a_1 ≠ 0
choose :
  ∀ (f : (a : α) → ι a) (hf : ∀ (a : α), x a (f a) ≠ 0),
    ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0
⊢ ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0

Tactic:
choose f hf using hx
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
f : (a : α) → ι a
hf : ∀ (a : α), x a (f a) ≠ 0
⊢ ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0

Tactic:
⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, Exists.intro
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
f : (a : α) → ι a
hf : ∀ (a : α), x a (f a) ≠ 0
⊢ ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0

Tactic:
exact ⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ Ne (α := ((a : α) → ι a) → K) (fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) 0

Tactic:
case h₁ =>
    simp_rw [ne_iff, Pi.zero_def] at hx ⊢
    choose f hf using hx
    exact ⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩

Premises used: Pi.zero_def, Function.ne_iff
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
simp_rw :
  HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (x_1 : AbsoluteValue K ℝ) ↦ ∏ a : α, ⨆ (i : ι a), (x_1 : (a : K) → ℝ) (x a i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ∏ a : α, ⨆ (i : ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
    ∏ a : α, mulHeight (x a)
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : (a : α) → ι a), (v : (a : K) → ℝ) (∏ a : α, x a (i a)))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : (a : α) → ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∏ a : α, x a (i a))) =
    ∏ a : α, mulHeight (x a)

Tactic:
simp_rw [_root_.map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass]

Premises used: map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
rw :
  Eq (α := ℝ)
    (∏ x_1 : α,
      HMul.hMul (α := ℝ)
        (Multiset.prod
          (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι x_1), (i : (a : K) → ℝ) (x x_1 i_1)) archAbsVal))
        (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι x_1), ((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x x_1 i)))
    (∏ a : α, mulHeight (x a))
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (x_1 : AbsoluteValue K ℝ) ↦ ∏ a : α, ⨆ (i : ι a), (x_1 : (a : K) → ℝ) (x a i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ∏ a : α, ⨆ (i : ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
    ∏ a : α, mulHeight (x a)

Tactic:
rw [Multiset.prod_map_prod,
    finprod_prod_comm _ _ fun b _ ↦ hasFiniteMulSupport_iSup_nonarchAbsVal (hx b),
    ← prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, finprod_prod_comm, _private.0.Height.hasFiniteMulSupport_iSup_nonarchAbsVal, Multiset.prod_map_prod
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
a : α
h : Membership.mem (γ := Finset α) univ a
rw rw₁ :
  HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι a), (i : (a : K) → ℝ) (x a i_1)) archAbsVal))
      (∏ᶠ (a_1 : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι a), ((↑a_1 : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι a), (v : (a : K) → ℝ) (x a i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i))
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι a), (i : (a : K) → ℝ) (x a i_1)) archAbsVal))
      (∏ᶠ (a_1 : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι a), ((↑a_1 : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
    mulHeight (x a)

Tactic:
rw [mulHeight_eq (hx a)]

Premises used: Height.mulHeight_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ Eq (α := ℝ)
    (∏ x_1 : α,
      HMul.hMul (α := ℝ)
        (Multiset.prod
          (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι x_1), (i : (a : K) → ℝ) (x x_1 i_1)) archAbsVal))
        (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι x_1), ((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x x_1 i)))
    (∏ a : α, mulHeight (x a))

Tactic:
exact prod_congr rfl fun a _ ↦ by rw [mulHeight_eq (hx a)]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
rw : log (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = log (∏ i : α, mulHeight (x i))
⊢ log (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = ∑ x_1 : α, log (mulHeight (x x_1))

Tactic:
rw [← log_prod fun a _ ↦ mulHeight_ne_zero _]

Premises used: Real.log_prod, Height.mulHeight_ne_zero
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ log (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = log (∏ i : α, mulHeight (x i))

Tactic:
congrArg log <| mulHeight_fun_prod_eq hx

Premises used: Height.mulHeight_fun_prod_eq, congrArg, Real.log
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ log (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = log (∏ i : α, mulHeight (x i))

Tactic:
exact congrArg log <| mulHeight_fun_prod_eq hx

Premises used: Height.mulHeight_fun_prod_eq, congrArg, Real.log
-- Module: Mathlib.NumberTheory.Height.Basic
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
obtain : ∀ (i : ι) (hi : x i ≠ 0 i), Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
⊢ Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0

Tactic:
obtain ⟨i, hi⟩ := 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
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
i : ι
hi : x i ≠ 0 i
obtain : ∀ (j : ι') (hj : y j ≠ 0 j), Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
⊢ Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0

Tactic:
obtain ⟨j, hj⟩ := ne_iff.mp hy

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
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
i : ι
hi : x i ≠ 0 i
j : ι'
hj : y j ≠ 0 j
⊢ Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0

Tactic:
ne_iff.mpr ⟨⟨i, j⟩, mul_ne_zero hi hj⟩

Premises used: Iff.mpr, Prod.mk, Function.ne_iff, Exists.intro, mul_ne_zero
-- Module: Mathlib.NumberTheory.Height.Basic
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
i : ι
hi : x i ≠ 0 i
j : ι'
hj : y j ≠ 0 j
⊢ Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0

Tactic:
exact ne_iff.mpr ⟨⟨i, j⟩, mul_ne_zero hi hj⟩

Premises used: Iff.mpr, Function.ne_iff, Exists.intro
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0

Tactic:
have hxy : (fun a : ι × ι' ↦ x a.1 * y a.2) ≠ 0 := by
    obtain ⟨i, hi⟩ := ne_iff.mp hx
    obtain ⟨j, hj⟩ := ne_iff.mp hy
    exact ne_iff.mpr ⟨⟨i, j⟩, mul_ne_zero hi hj⟩
-- Module: Mathlib.NumberTheory.Height.Basic
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
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)))
⊢ (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = mulHeight x * mulHeight y

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)]

Premises used: mul_mul_mul_comm, finprod_mul_distrib, Multiset.prod_map_mul, _private.0.Height.hasFiniteMulSupport_iSup_nonarchAbsVal, 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
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))
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))
⊢ 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:
congr
-- Module: Mathlib.NumberTheory.Height.Basic
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 :
  ∀ (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))
⊢ 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:
ext1 v
-- Module: Mathlib.NumberTheory.Height.Basic
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 :
  ∀ (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))
⊢ 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:
ext1 v
-- Module: Mathlib.NumberTheory.Height.Basic
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
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:
Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v x y

Premises used: Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg
-- Module: Mathlib.NumberTheory.Height.Basic
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
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:
exact Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v x y

Premises used: Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg
-- Module: Mathlib.NumberTheory.Height.Basic
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
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:
Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v.val x y

Premises used: Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg, Subtype.val
-- Module: Mathlib.NumberTheory.Height.Basic
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
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:
exact Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v.val x y

Premises used: Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg, Subtype.val
-- Module: Mathlib.NumberTheory.Height.Basic
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
pull : log (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = log (mulHeight x * mulHeight y)
⊢ log (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = log (mulHeight x) + log (mulHeight y)

Tactic:
pull (disch := positivity) log

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
rw rw₁ : log (mulHeight x * mulHeight y) = log (mulHeight x * mulHeight y)
⊢ log (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = log (mulHeight x * mulHeight y)

Tactic:
rw [mulHeight_fun_mul_eq hx hy]

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
x : ι → K
inl : mulHeight.{u_1, u_2} (K := K) (ι := ι) (-0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
inr : ∀ (hx : x ≠ 0), mulHeight (-x) = mulHeight x
⊢ mulHeight (-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
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) (-0) = mulHeight.{u_1, u_2} (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
x : ι → K
hx : x ≠ 0
⊢ mulHeight (-x) = mulHeight x

Tactic:
simp [mulHeight_eq hx, mulHeight_eq <| neg_ne_zero.mpr hx]

Premises used: Iff.mpr, Height.mulHeight_eq, neg_ne_zero
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
⊢ logHeight (-x) = logHeight x

Tactic:
simp [logHeight_eq_log_mulHeight]

Premises used: Height.logHeight_eq_log_mulHeight