awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
a : ℂ
ha : 0 < a.re
h₁ :
  Membership.mem («γ» := Set ℂ) {1}ᶜ a →
    HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
⊢ Membership.mem («γ» := Set ℂ) {1}ᶜ a →
    HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)

Tactic:
_
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
h₁ :
  ∀ (a : ℂ) (ha : 0 < a.re),
    Membership.mem («γ» := Set ℂ) {1}ᶜ a →
      HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
⊢ ∀ᶠ (x : ℂ) in 𝓝 1,
    Membership.mem («γ» := Set ℂ) {1}ᶜ x →
      HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)

Tactic:
filter_upwards [this] with a ha _
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
a : ℂ
ha : 0 < a.re
h_1 : Membership.mem («γ» := Set ℂ) {1}ᶜ a
h₁ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
h₂ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = (1 - 1 / a.Gammaℝ) / (a - 1)
h₃ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (1 - 1 / a.Gammaℝ) / (a - 1)
h₄ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (1 * a.Gammaℝ - 1) / a.Gammaℝ / (a - 1)
h₅ h₆ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1)
⊢ HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)

Tactic:
rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]

Premises used: div_right_comm, sub_div, Pi.div_apply, Complex.Gammaℝ_ne_zero_of_re_pos, sub_div', one_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))

Tactic:
have := tendsto_riemannZeta_sub_one_div.add tendsto_Gamma_term_aux
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this :
  Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))

Tactic:
simp_rw [sub_add_sub_cancel] at this

Premises used: sub_add_sub_cancel
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this :
  Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))

Tactic:
this
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this :
  Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
h : ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 = (↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2))

Tactic:
convert! this using 2
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this :
  Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 = (↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ Tendsto (fun (s : ℂ) ↦ HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1)
    (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))

Tactic:
have := (HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one 0).mono_left
    <| nhdsWithin_le_nhds (s := {1}ᶜ)
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this :
  Tendsto (fun (s : ℂ) ↦ HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1)
    (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))

Tactic:
simp only [HurwitzZeta.hurwitzZetaEven_zero, div_right_comm _ _ (Gammaℝ _)] at this

Premises used: div_right_comm, HurwitzZeta.hurwitzZetaEven_zero, Complex.Gammaℝ
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))
⊢ riemannZeta 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2

Tactic:
tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_Gammaℝ

Premises used: ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ, tendsto_nhds_unique
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))
⊢ riemannZeta 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2

Tactic:
exact tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_Gammaℝ

Premises used: ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ, tendsto_nhds_unique
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / HSub.hSub (α := ℂ) 1 1

Tactic:
have := completedRiemannZeta_eq 1
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / HSub.hSub (α := ℂ) 1 1
⊢ completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1

Tactic:
rw [sub_self, div_zero, div_one, sub_zero, eq_sub_iff_add_eq] at this

Premises used: sub_self, sub_zero, eq_sub_iff_add_eq, div_one, div_zero
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
rw : completedRiemannZeta 1 + 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
rw₁ rw₂ : ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
⊢ completedRiemannZeta₀ 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1

Tactic:
rw [← this, completedRiemannZeta_one]

Premises used: completedRiemannZeta_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ 0 ≤ 4 * π

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ riemannZeta 1 ≠ 0

Tactic:
simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π),
      push_cast]

Premises used: Complex.ofReal_log, Complex.ofReal_ne_zero, riemannZeta_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
suffices : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ riemannZeta 1 ≠ 0

Tactic:
suffices (γ - (4 * π).log) / 2 ≠ 0 by
    simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π),
      push_cast]
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ (γ - Real.log (4 * π)) / 2 ≠ 0

Tactic:
div_ne_zero (sub_lt_zero.mpr (lt_trans ?_ ?_ (b := 1))).ne two_ne_zero

Premises used: Iff.mpr, sub_lt_zero, lt_trans, div_ne_zero, two_ne_zero, LT.lt.ne
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
refine_1 : γ < 1
refine_2 : 1 < Real.log (4 * π)
⊢ (γ - Real.log (4 * π)) / 2 ≠ 0

Tactic:
refine div_ne_zero (sub_lt_zero.mpr (lt_trans ?_ ?_ (b := 1))).ne two_ne_zero

Premises used: div_ne_zero, two_ne_zero
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ 2 / 3 < 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ γ < 1

Tactic:
exact Real.eulerMascheroniConstant_lt_two_thirds.trans (by norm_num)

Premises used: Real.eulerMascheroniConstant_lt_two_thirds, LT.lt.trans
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ 0 < 4 * π

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
refine_2 : rexp 1 < 4 * π
⊢ 1 < Real.log (4 * π)

Tactic:
rw [lt_log_iff_exp_lt (by positivity)]

Premises used: Real.lt_log_iff_exp_lt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ 2.7182818286 < HMul.hMul (α := ℝ) 4 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ LE.le (α := ℝ) 0 4

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ rexp 1 < 4 * π

Tactic:
exact (lt_trans Real.exp_one_lt_d9 (by norm_num)).trans_le
      <| mul_le_mul_of_nonneg_left two_le_pi (by simp)

Premises used: Real.two_le_pi, lt_trans, LT.lt.trans_le, Real.exp_one_lt_d9, mul_le_mul_of_nonneg_left
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : ∀ (a : ℂ), (Membership.mem («γ» := Set ℂ) {1}ᶜ a → (a - 1) * riemannZeta a ≠ 0) → riemannZeta a ≠ 0
⊢ ∀ᶠ (s : ℂ) in 𝓝 1, riemannZeta s ≠ 0

Tactic:
filter_upwards [eventually_nhdsWithin_iff.1 <| riemannZeta_residue_one.eventually_ne one_ne_zero]

Premises used: Filter.Tendsto.eventually_ne, eventually_nhdsWithin_iff, Iff.mp, riemannZeta_residue_one, one_ne_zero
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ ∀ (a : ℂ), (Membership.mem («γ» := Set ℂ) {1}ᶜ a → (a - 1) * riemannZeta a ≠ 0) → riemannZeta a ≠ 0

Tactic:
grind [riemannZeta_one_ne_zero]

Premises used: riemannZeta_one_ne_zero
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x =
    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)

Tactic:
rfl

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

Tactic:
simp [mulHeight₁_eq]

Premises used: Height.mulHeight₁_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
⊢ mulHeight₁.{u_1} (K := K) 1 = 1

Tactic:
simp [mulHeight₁_eq]

Premises used: Height.mulHeight₁_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ 1 ≤ mulHeight₁ x

Tactic:
one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod_map fun _ _ ↦ le_max_right ..) <|
    one_le_finprod fun _ ↦ le_max_right ..

Premises used: le_max_right, one_le_finprod, Height.mulHeight₁, Multiset.one_le_prod_map, OfNat.ofNat, Subtype.val, DFunLike.coe, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ 0 < mulHeight₁ x

Tactic:
zero_lt_one.trans_le <| one_le_mulHeight₁ x

Premises used: Height.one_le_mulHeight₁, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x ≠ 0

Tactic:
(mulHeight₁_pos x).ne'

Premises used: Height.mulHeight₁_pos, LT.lt.ne'
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ 0 ≤ mulHeight₁ x

Tactic:
(mulHeight₁_pos x).le

Premises used: LT.lt.le, Height.mulHeight₁_pos
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
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
⊢ logHeight₁.{u_1} (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
⊢ logHeight₁.{u_1} (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
x : K
⊢ 0 ≤ logHeight₁ x

Tactic:
Real.log_nonneg <| one_le_mulHeight₁ x

Premises used: Height.logHeight₁, Height.one_le_mulHeight₁, Real.log_nonneg
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x ≠ 0

Tactic:
have H : mulHeight₁ x ≠ 0 := mulHeight₁_ne_zero x
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H : mulHeight₁ x ≠ 0
⊢ 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

Tactic:
rw [mulHeight₁_eq] at H

Premises used: Height.mulHeight₁_eq
-- Module: Mathlib.NumberTheory.Height.Basic
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
a : ℝ
ha :
  Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal)
    a
contrapose : ∀ (ha : a = 0), a ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal
⊢ a ≠ 0

Tactic:
contrapose ha
-- Module: Mathlib.NumberTheory.Height.Basic
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
a : ℝ
ha : a = 0
rw : 0 ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal
⊢ a ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal

Tactic:
rw [ha]
-- Module: Mathlib.NumberTheory.Height.Basic
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
a : ℝ
ha : a = 0
⊢ 0 ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal

Tactic:
Multiset.prod_eq_zero_iff.not.mp <| left_ne_zero_of_mul H

Premises used: Multiset.prod_eq_zero_iff, Iff.not, left_ne_zero_of_mul, Iff.mp
-- Module: Mathlib.NumberTheory.Height.Basic
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
a : ℝ
ha : a = 0
⊢ 0 ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal

Tactic:
exact Multiset.prod_eq_zero_iff.not.mp <| left_ne_zero_of_mul H

Premises used: Multiset.prod_eq_zero_iff, Iff.not, left_ne_zero_of_mul, Iff.mp
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ ∀ (a : ℝ),
    Membership.mem (γ := Multiset ℝ)
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal) a →
      a ≠ 0

Tactic:
have : ∀ a ∈ archAbsVal.map (fun v ↦ max (v x) 1), a ≠ 0 := by
    intro a ha
    contrapose ha
    rw [ha]
    exact Multiset.prod_eq_zero_iff.not.mp <| left_ne_zero_of_mul H
-- Module: Mathlib.NumberTheory.Height.Basic
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
x_1 : (↑nonarchAbsVal : Type u_1)
⊢ LT.lt (α := ℝ) (0 : ℝ) (max (((↑x_1 : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1 : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.Basic
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
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))
⊢ 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))

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

Premises used: right_ne_zero_of_mul, left_ne_zero_of_mul, Real.log_multiset_prod, Multiset.map_map, Real.log_finprod, Real.log_mul
-- Module: Mathlib.NumberTheory.Height.Basic
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)
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)
⊢ 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:
congr 2
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ 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:
simp [max_comm, posLog_eq_log_max_one]

Premises used: Real.posLog_eq_log_max_one, max_comm
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ 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:
simp [max_comm, posLog_eq_log_max_one]

Premises used: Real.posLog_eq_log_max_one, max_comm
-- 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 =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))

Tactic:
simp [mulHeight, hx]

Premises used: Height.mulHeight
-- 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 = 1

Tactic:
simp [mulHeight]

Premises used: Height.mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
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
inr : ∀ (hι : Nonempty ι), mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1
⊢ mulHeight.{u_1, u_2} (K := K) (ι := ι) 1 = 1

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

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

Tactic:
rw [show (1 : ι → K) = 0 from Subsingleton.elim ..]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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:
mulHeight_zero

Premises used: Height.mulHeight_zero