mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
wlog hd : 0 ≤ g 1 1
  · specialize this hz (g := -g) (SL_neg_smul g z ▸ hg) (by simpa using hc) ?_
    · simpa using (not_le.mp hd).le
    convert! this using 2 <;> simp [neg_eq_iff_eq_neg, or_comm]
  have hd' : g 1 1 = 1 ∨ g 1 1 = -1 := by
    simpa [hc, isCoprime_zero_left, Int.isUnit_iff] using bottom_row_coprime g
  replace hd : g 1 1 = 1 := by grind
  have ha : g 0 0 = 1 := by grind [det_fin_two, g.property]
  let b := g 0 1
  have hgz : g = T ^ b := by
    ext i j
    rw [coe_T_zpow]
    fin_cases i <;> fin_cases j <;> tauto
  have hre : (g • z).re = b + z.re := by
    rw [hgz, ← coe_re, coe_T_zpow_smul_eq, add_re, coe_re, intCast_re, add_comm]
  have := (abs_sub_abs_le_abs_add ..).trans (hre ▸ hg.2)
  grw [sub_le_iff_le_add, hz.2, add_halves, ← Int.cast_abs, ← Int.cast_one, Int.cast_le,
    Int.abs_le_one_iff] at this
  rcases this with hb | hb | hb <;> rw [hb] at hgz
  · rw [hgz]
    simp
  · left
    rw [hgz, zpow_one, eq_self_iff_true, true_or, true_and]
    rw [hb, Int.cast_one] at hre
    linarith [(le_abs_self _).trans (abs_neg z.re ▸ hz.2), (le_abs_self _).trans hg.2]
  · right
    left
    rw [hgz, zpow_neg_one, eq_self_iff_true, true_or, true_and]
    rw [hb, Int.cast_neg, Int.cast_one] at hre
    linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑(f - (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • g)) = 0

Tactic:
FunLike.coe_sub,

Goal state after:
k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (PowerSeries.coeff 0) (qExpansion 1 (⇑f - ⇑((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • g))) = 0
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℍ
⊢ logDeriv η ↑z = ↑π * I / 12 * E2 z

Tactic:
by
  unfold eta
  rw [logDeriv_mul _ (Periodic.qParam_ne_zero _) (eta_tprod_ne_zero z.2) (by fun_prop)
    (differentiableAt_eta_tprod z.2)]
  have HG := logDeriv_tprod_eq_tsum isOpen_upperHalfPlaneSet z.2
    (one_sub_eta_q_ne_zero · z.2) (by fun_prop) (summable_logDeriv_one_sub_eta_q z.2)
    multipliableLocallyUniformlyOn_eta (eta_tprod_ne_zero z.2)
  simp only [logDeriv_qParam 24 z, HG, tsum_logDeriv_eta_q z, E2, one_div,
    mul_inv_rev, Pi.smul_apply, smul_eq_mul]
  rw [G2_eq_tsum_cexp, riemannZeta_two, ← tsum_pow_div_one_sub_eq_tsum_sigma
    (norm_exp_two_pi_I_lt_one z), mul_sub, sub_eq_add_neg, mul_add]
  simp [eta_q_eq_pow, ← tsum_mul_left, tsum_pnat_eq_tsum_succ (f := fun n ↦
        n * cexp (2 * π * I * z) ^ n / (1 - cexp (2 * π * I * z) ^ n)), ← tsum_neg]
  grind

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
x : ℕ
⊢ ∑' (n : ℤ), ∑ m ∈ Finset.Ico (-↑x) ↑x, 1 / (↑n * ↑z + ↑m) ^ 2 =
    ∑ n ∈ Finset.Ico (-↑x) ↑x, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2

Tactic:
Summable.tsum_finsetSum (fun i hi ↦ ?_)

Goal state after:
z : ℍ
x : ℕ
⊢ ∑ i ∈ Finset.Ico (-↑x) ↑x, ∑' (b : ℤ), 1 / (↑b * ↑z + ↑i) ^ 2 =
    ∑ n ∈ Finset.Ico (-↑x) ↑x, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2

z : ℍ
x : ℕ
i : ℤ
hi : i ∈ Finset.Ico (-↑x) ↑x
⊢ Summable fun n ↦ 1 / (↑n * ↑z + ↑i) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      (-D2 g) ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹

Tactic:
SlashAction.neg_slash

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
x : ↑K
h1 : cexp (2 * ↑π * I * (↑x / ↑p)) = cexp (2 * ↑π * I * ↑x / ↑p)
⊢ ‖cexp (2 * ↑π * I * ↑x / ↑p)‖ < 1

Tactic:
simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h : Submodule.Quotient.mk (E hk) = 0
⊢ False

Tactic:
have hE := E_qExpansion_coeff_zero hk hk2

Goal state after:
case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h : Submodule.Quotient.mk (E hk) = 0
hE : (PowerSeries.coeff 0) (qExpansion 1 ⇑(E hk)) = 1
⊢ False
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • E hk - f)) = 0

Tactic:
FunLike.coe_sub,

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 (⇑((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • E hk) - ⇑f)) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ
⊢ (↑z ^ 2)⁻¹ * ∑ x ∈ Ico (-↑N) ↑N, ∑' (n : ℤ), ((-(↑x * (↑z)⁻¹) + ↑n) ^ 2)⁻¹ =
    ∑' (n : ℤ), ∑ x ∈ Ico (-↑N) ↑N, ((↑n * ↑z + ↑x) ^ 2)⁻¹

Tactic:
mul_sum,

Goal state after:
z : ℍ
N : ℕ
⊢ ∑ i ∈ Ico (-↑N) ↑N, (↑z ^ 2)⁻¹ * ∑' (n : ℤ), ((-(↑i * (↑z)⁻¹) + ↑n) ^ 2)⁻¹ =
    ∑' (n : ℤ), ∑ x ∈ Ico (-↑N) ↑N, ((↑n * ↑z + ↑x) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
apply (summable_pow_mul_cexp k 1 z).congr

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∀ (b : ℕ), ↑b ^ k * cexp (2 * ↑π * I * ↑↑1 * ↑z) ^ b = ↑b ^ k * cexp (2 * ↑π * I * ↑z) ^ b
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℤ), ∑ m ∈ Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) atTop
    (𝓝 (∑'[symmetricIco ℤ] (x : ℤ), (↑z ^ 2)⁻¹ * e2Summand x (S • z)))

Tactic:
have := ((summable_e2Summand_symmetricIco (S • z)).mul_left (z.1 ^ 2)⁻¹).hasSum

Goal state after:
z : ℍ
this :
  HasSum (fun i ↦ (↑z ^ 2)⁻¹ * e2Summand i (S • z)) (∑'[symmetricIco ℤ] (b : ℤ), (↑z ^ 2)⁻¹ * e2Summand b (S • z))
    (symmetricIco ℤ)
⊢ Tendsto (fun N ↦ ∑' (n : ℤ), ∑ m ∈ Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) atTop
    (𝓝 (∑'[symmetricIco ℤ] (x : ℤ), (↑z ^ 2)⁻¹ * e2Summand x (S • z)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑n) atTop (𝓝 0)

Tactic:
have := tendsto_zero_geometric_tsum_pnat (norm_exp_two_pi_I_lt_one ⟨_, im_pnat_div_pos 1 z⟩)

Goal state after:
z : ℍ
this : Tendsto (fun m ↦ ∑' (n : ℕ+), cexp (2 * ↑π * I * ↑{ coe := -↑1 / ↑z, coe_im_pos := ⋯ }) ^ (↑n * ↑m)) atTop (𝓝 0)
⊢ Tendsto (fun N ↦ ∑' (n : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑n) atTop (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
⊢ ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
    ∑' (m : ℤ), ∑ n ∈ Ico (-↑↑N) ↑↑N, (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))

Tactic:
Summable.tsum_finsetSum (fun i hi ↦ ?_)

Goal state after:
z : ℍ
N : ℕ+
⊢ ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
    ∑ i ∈ Ico (-↑↑N) ↑↑N, ∑' (b : ℤ), (1 / (↑b * ↑z + ↑i) - 1 / (↑b * ↑z + ↑i + 1))

z : ℍ
N : ℕ+
i : ℤ
hi : i ∈ Ico (-↑↑N) ↑↑N
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑i) - 1 / (↑m * ↑z + ↑i + 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
x : ℍ
hx✝ : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
hx : 1 = ‖↑x‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
exact mem_closure_of_arc hx.symm hx'

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ HasSum (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1)) ((E hk) τ - 1)

Tactic:
rw [hval]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ HasSum (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1))
    (β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: ⊢ qExpansion 1 ⇑E₄CubeSubE₆SqForm =
    qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆

Tactic:
simp only [E₄CubeSubE₆SqForm, FunLike.coe_sub, coe_mcast,
    ModularForm.qExpansion_sub one_pos one_mem_strictPeriods_SL,
    ModularForm.qExpansion_pow one_pos one_mem_strictPeriods_SL]
  ring

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))

Tactic:
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (((2 * ↑π) ^ (-s))⁻¹ / Gamma s * ↑(h Γ) ^ (-s))

Tactic:
cpow_neg (2 * _),

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (((2 * ↑π) ^ s)⁻¹⁻¹ / Gamma s * ↑(h Γ) ^ (-s))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hxy
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ↑p ∣ (∑ i ∈ range (p ^ multiplicity p (n + 1)), x ^ i * y ^ (p ^ multiplicity p (n + 1) - 1 - i)) * (x - y)

Tactic:
exact dvd_mul_of_dvd_right hxy

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hx
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ ¬2 ∣ x ^ 2 ^ multiplicity 2 (n + 1)

pp: case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ ¬2 ∣ ↑k

Tactic:
· simpa only [even_iff_two_dvd, ← Int.not_even_iff_odd] using hx_odd.pow

Goal state after:
case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ ¬2 ∣ ↑k
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.FiniteIndex

Tactic:
rw [Subgroup.finiteIndex_iff, ← Subgroup.relIndex_mul_index (le_sup_left : s ≤ s ⊔ torsion K)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (s ⊔ torsion K) * (s ⊔ torsion K).index ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝ : mixedSpace K
⊢ 1 • x✝ = x✝

Tactic:
simp_rw [unitSMul_smul, Units.coe_one, map_one, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ 0 < regOfFamily u

Tactic:
classical
  rw [regOfFamily_of_isMaxRank hu]
  exact ZLattice.covolume_pos _ volume

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ y ∈ fundamentalCone K

Tactic:
by
  refine ⟨?_, by simpa [norm_eq_of_normAtPlace_eq hy] using hx.2⟩
  rw [Set.mem_preimage, logMap_eq_of_normAtPlace_eq hy]
  exact hx.1

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ (algebraMap K w.Completion) x = completionMap { toCompletion := ↑(WithAbs.toAbs (↑v) x) }

Tactic:
completionMap_coe

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ (algebraMap K w.Completion) x = { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) (WithAbs.toAbs (↑v) x)) }
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inr.inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
have : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding := ⟨hr⟩
      have := liesOver_conjugate_extensionEmbedding w v
      rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
        ((ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)).trans
          (starRingAut (R := ℂ))) (by ext; simp [← conjugate_coe_eq]),
        Module.finrank_self]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun i ↦
      Real.exp (x w₀) *
        (∏ x_1,
            normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1)))) ^
              x ↑x_1)
          i) =
    fun i ↦ Real.exp (x w₀) * ∏ i_1, i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i_1))) ^ x ↑i_1

Tactic:
prod_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun i ↦
      Real.exp (x w₀) *
        ∏ c,
          (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm c)))) ^ x ↑c)
            i) =
    fun i ↦ Real.exp (x w₀) * ∏ i_1, i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i_1))) ^ x ↑i_1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ∈ ↑expMapBasis '' closure (paramSet K)

Tactic:
refine ⟨fun w ↦ if w = w₀ then Real.log c else y w, ?_, ?_⟩

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ (fun w ↦ if w = w₀ then Real.log c else y w) ∈ closure (paramSet K)

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ (↑expMapBasis fun w ↦ if w = w₀ then Real.log c else y w) = (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ 0 < c

Tactic:
contrapose! hx₀

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : c ≤ 0
⊢ c • ↑expMapBasis y = 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))

Tactic:
rw [← Nat.totient_prime hp.out, ← hζ.toInteger_isPrimitiveRoot.card_primitiveRoots,
    ← Finset.prod_const]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated (∏ _x ∈ primitiveRoots p (𝓞 K), (hζ.toInteger - 1)) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : ¬x = 0
⊢ x ∈ compactSet K ↔ x ∈ ↑expMapBasis '' closure (paramSet K) ∪ {0}

Tactic:
refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩
    simp only [Set.union_singleton, Set.mem_insert_iff, hx₀, false_or] at hx
    exact compactSet_eq_union_aux₂ hx₀ hx

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    (MeasureTheory.volume (⇑(toMixed K) ⁻¹' normLeOne K)).toReal /
        ZLattice.covolume (ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) ↑↑(toMixed K))
          MeasureTheory.volume *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)

Tactic:
(volumePreserving_toMixed K).measure_preimage
      (measurableSet_normLeOne K).nullMeasurableSet,

Goal state after:
case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    (MeasureTheory.volume (normLeOne K)).toReal /
        ZLattice.covolume (ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) ↑↑(toMixed K))
          MeasureTheory.volume *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f ↑x.num.natAbs ^ c / g ↑x.den = g ↑x.num.natAbs / g ↑x.den

Tactic:
h (natAbs x.num)

Goal state after:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ g ↑x.num.natAbs / g ↑x.den = g ↑x.num.natAbs / g ↑x.den
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inr
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
n : ℕ
hn : n ≠ 0
⊢ f ↑n = AbsoluteValue.trivial ↑n

Tactic:
simp [hf_nontriv, hn]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
remark :
  ∀ (α : 𝓞 K) (i : K →+* ℂ),
    |↑(((RingOfIntegers.basis K).repr α) ((equivReindex K).symm.symm i))| ≤ c K * house ((algebraMap (𝓞 K) K) α)
⊢ ↑|asiegel K a kr lu| ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (newBasis K) lu.2))

Tactic:
exact mod_cast remark ((a kr.1 lu.1 * ((newBasis K) lu.2))) kr.2

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun i ↦ f i.1 * g i.2) (a * b)

Tactic:
by
  rw [← hasSum_iff_hasSum_compl] at *
  simp only [Function.comp_def, UniformSpace.Completion.toCompl_apply,
    UniformSpace.Completion.coe_mul]
  exact (hf.mul hg) (hf.summable.mul_of_complete_nonarchimedean hg.summable :)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case hbc
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) ≤ A

Tactic:
exact habs kr.1 lu.1

Goal state after: