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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsZeroAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
IsZeroAtImInfty,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ atImInfty.ZeroAtFilter ((c • f.toSlashInvariantForm).toFun ∣[k] g)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsZeroAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
IsZeroAtImInfty,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ atImInfty.ZeroAtFilter ((c • f.toSlashInvariantForm).toFun ∣[k] g)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|

Tactic:
by
  have : Nonempty { g : SL(2, ℤ) // g 1 = cd } :=
    let ⟨x, hx⟩ := bottom_row_surj hcd
    ⟨⟨x, hx.2⟩⟩
  obtain ⟨g, hg⟩ := Filter.Tendsto.exists_forall_le (tendsto_abs_re_smul z hcd)
  refine ⟨g, g.2, ?_⟩
  intro g1 hg1
  have : g1 ∈ (fun g : SL(2, ℤ) => g 1) ⁻¹' {cd} := by
    rw [Set.mem_preimage, Set.mem_singleton_iff]
    exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2))
  exact hg ⟨g1, this⟩

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ IsZeroAtImInfty fun τ ↦ ‖petersson k (⇑f) (⇑f') (g • τ)‖

Tactic:
IsZeroAtImInfty,

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ atImInfty.ZeroAtFilter fun τ ↦ ‖petersson k (⇑f) (⇑f') (g • τ)‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
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.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
m : ℕ+
⊢ ‖r ^ ↑m‖ < 1

Tactic:
rwa [norm_pow, pow_lt_one_iff_of_nonneg (norm_nonneg _) (NeZero.ne _)]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ IsZeroAtImInfty ⇑f

Tactic:
IsZeroAtImInfty,

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ atImInfty.ZeroAtFilter ⇑f
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S * T)

Tactic:
coe_mul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S) * ↑T
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S) * ↑T

Tactic:
coe_mul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g = ↑(T ^ ↑g 0 0) * ↑S * ↑T
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
⊢ (T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T) ∧ z = ρ

Tactic:
have hρ : z = ρ := by
    apply eq_of_re_of_norm
    · simp [hre, ρ]
    · rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ (T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T) ∧ z = ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S * T⁻¹)

Tactic:
coe_mul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S) * ↑T⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S) * ↑T⁻¹

Tactic:
coe_mul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0) * ↑S * ↑T⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
N : ℤ
⊢ ∑' (b : ℤ), (1 / (↑b * ↑z + ↑N) ^ 2 - (1 / (↑b * ↑z + ↑N) - 1 / (↑b * ↑z + ↑N + 1))) = ∑' (m : ℤ), G2Term z ![m, N]

Tactic:
apply tsum_congr (fun M ↦ ?_)
      simp only [one_div, G2Term, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
        Matrix.cons_val_fin_one, mul_inv_rev]
      nth_rw 1 [← aux_identity z M N]
      ring

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

Goal state before:
pp: case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]

pp: case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
· exact (G2Term_prod_summable z).prod_factor

Goal state after:
case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case h
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ

Tactic:
exact fun n _ _ ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cexp n

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

Goal state before:
pp: case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
b : ℕ+
⊢ I ^ 2 * ↑π ^ 2 * ↑↑b * cexp (I * ↑π * ↑z * ↑a * ↑↑b * 2 + I * ↑π * ↑z * ↑↑b * 2) * 8 =
    -(↑π ^ 2 * ↑↑b * cexp (I * ↑π * ↑z * ↑↑b * 2) * cexp (I * ↑π * ↑z * ↑↑b * ↑a * 2) * 8)

Tactic:
grind [I_sq, exp_add]

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

Goal state before:
pp: z : ℍ
this :
  ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ 1 * cexp (2 * ↑π * I * ↑z) ^ (↑d * ↑c) =
    ∑' (e : ℕ+), ↑((σ 1) ↑e) * cexp (2 * ↑π * I * ↑z) ^ ↑e
⊢ -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
rw [tsum_pnat_eq_tsum_succ (f := fun d ↦ ∑' c : ℕ+, c ^ 1 * 𝕢 z ^ (d * c : ℕ))] at this

Goal state after:
z : ℍ
this :
  ∑' (n : ℕ) (c : ℕ+), ↑↑c ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ((n + 1) * ↑c) =
    ∑' (e : ℕ+), ↑((σ 1) ↑e) * cexp (2 * ↑π * I * ↑z) ^ ↑e
⊢ -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case ha
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑a ≠ 0

pp: case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0

Tactic:
· simpa using linear_ne_zero z (cd := ![m, a]) (by aesop)

Goal state after:
case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
⊢ IsCompact {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
Metric.isCompact_iff_isClosed_bounded

Goal state after:
y : ℝ
⊢ IsClosed {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} ∧
    Bornology.IsBounded {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsZeroAtImInfty ((∑ q, quotientFunc f q) ∣[k] γ)

Tactic:
IsZeroAtImInfty,

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ atImInfty.ZeroAtFilter ((∑ q, quotientFunc f q) ∣[k] γ)
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
⊢ ∑ i ∈ range p,
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a + ↑p * b) ^ i * (Ideal.Quotient.mk (span {↑p ^ 2})) a ^ (p - 1 - i) =
    ∑ x ∈ range p, (Ideal.Quotient.mk (span {↑p ^ 2})) ((a ^ (x - 1) * (↑p * b) * ↑x + a ^ x) * a ^ (p - 1 - x))

Tactic:
← map_pow,

Goal state after:
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
⊢ ∑ x ∈ range p,
      (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ x) * (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 1 - x)) =
    ∑ x ∈ range p, (Ideal.Quotient.mk (span {↑p ^ 2})) ((a ^ (x - 1) * (↑p * b) * ↑x + a ^ x) * a ^ (p - 1 - x))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ ¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)

Tactic:
dvd_iff_dvd_of_dvd_sub hxy

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ y
⊢ ¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J

Tactic:
idealSetMap,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ ↑(preimageOfMemIntegerSet ⟨↑a, ⋯⟩) ∈ ↑↑J
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ normAtAllPlaces '' normLeOne K =
    ⇑mixedSpaceOfRealSpace ⁻¹'
            logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∩
          {x | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩
        {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0} ∩
      {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}

Tactic:
by
  ext x
  refine ⟨?_, fun ⟨⟨⟨h₁, h₂⟩, h₃⟩, h₄⟩ ↦ ?_⟩
  · rintro ⟨y, ⟨⟨h₁, h₂⟩, h₃⟩, rfl⟩
    refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
    · rwa [Set.mem_preimage, ← logMap_normAtAllPlaces] at h₁
    · exact fun w ↦ normAtPlace_nonneg w y
    · rwa [Set.mem_ofPred_eq, ← norm_normAtAllPlaces] at h₂
    · rwa [Set.mem_ofPred_eq, ← norm_normAtAllPlaces] at h₃
  · exact ⟨mixedSpaceOfRealSpace x, ⟨⟨h₁, h₃⟩, h₄⟩, normAtAllPlaces_mixedSpaceOfRealSpace h₂⟩

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)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    ↑(finrank ℚ K) *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|

Tactic:
regOfFamily_eq_det u w' e,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e i))))).det| =
    ↑(finrank ℚ K) *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this✝ : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero ↑n
⊢ False

Tactic:
have hP : P ∈ normalizedFactors (cyclotomic n K) := count_pos.mp (by lia)

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this✝ : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero ↑n
hP : P ∈ normalizedFactors (cyclotomic n K)
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : realSpace K) in ↑expMapBasis '' s, f x =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
          f (↑expMapBasis x)

Tactic:
rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume hs
    (fun x _ ↦ (hasFDerivAt_expMapBasis K x).hasFDerivWithinAt) (injective_expMapBasis K).injOn]
  simp_rw [abs_det_fderiv_expMapBasis]
  have : Measurable expMapBasis := (continuous_expMapBasis K).measurable
  rw [← lintegral_const_mul _ (by fun_prop)]
  congr with x
  have : 0 ≤ (∏ w : {w // IsComplex w}, expMapBasis x w.1)⁻¹ :=
    inv_nonneg.mpr <| Finset.prod_nonneg fun _ _ ↦ (expMapBasis_pos _ _).le
  rw [ofReal_mul (by positivity), ofReal_mul (by positivity), ofReal_mul (by positivity),
    ofReal_mul (by positivity), ofReal_pow (by positivity), ofReal_inv_of_pos (Finset.prod_pos
    fun _ _ ↦ expMapBasis_pos _ _), ofReal_inv_of_pos zero_lt_two, ofReal_ofNat, ofReal_natCast,
    ofReal_prod_of_nonneg (fun _ _ ↦ (expMapBasis_pos _ _).le)]
  ring

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ normAtAllPlaces '' normLeOne K = ↑expMapBasis '' paramSet K

Tactic:
ext x
  by_cases hx : ∀ w, 0 < x w
  · rw [← expMapBasis.right_inv (Set.mem_univ_pi.mpr hx), (injective_expMapBasis K).mem_set_image]
    simp only [normAtAllPlaces_normLeOne, Set.mem_inter_iff, Set.mem_ofPred_eq, expMapBasis_nonneg,
      Set.mem_preimage, logMap_expMapBasis, implies_true, and_true, norm_expMapBasis,
      pow_le_one_iff_of_nonneg (Real.exp_nonneg _) Module.finrank_pos.ne', Real.exp_le_one_iff,
      ne_eq, pow_eq_zero_iff', Real.exp_ne_zero, false_and, not_false_eq_true, Set.mem_univ_pi]
    refine ⟨fun ⟨h₁, h₂⟩ w ↦ ?_, fun h ↦ ⟨fun w hw ↦ by simpa [hw] using h w, by simpa using h w₀⟩⟩
    · split_ifs with hw
      · exact hw ▸ h₂
      · exact h₁ w hw
  · refine ⟨?_, ?_⟩
    · rintro ⟨a, ⟨ha, _⟩, rfl⟩
      exact (hx fun w ↦ fundamentalCone.normAtPlace_pos_of_mem ha w).elim
    · rintro ⟨a, _, rfl⟩
      exact (hx fun w ↦ expMapBasis_pos a w).elim

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: case hx
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ (algebraMap F K) ζ ^ n = 1

Tactic:
← map_pow,

Goal state after:
case hx
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ (algebraMap F K) (ζ ^ n) = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : x ∈ ↑expMapBasis '' closure (paramSet K)
⊢ x ∈ compactSet K

Tactic:
classical
  simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
  obtain ⟨y, hy, rfl⟩ := hx₁
  refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
  · exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))
  · split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)

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

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ P.inertiaDeg ℤ = orderOf ↑p

Tactic:
by
  replace hm : p.Coprime m := hp.out.coprime_iff_not_dvd.mpr hm
  let ζ := (zeta_spec m ℚ K).toInteger
  have h₁ : ¬ p ∣ exponent ζ := by
    rw [exponent_eq_one_iff.mpr <| adjoin_singleton_eq_top (zeta_spec m ℚ K)]
    exact hp.out.not_dvd_one
  have h₂ := (primesOverSpanEquivMonicFactorsMod h₁ ⟨P, ⟨inferInstance, inferInstance⟩⟩).2
  have h₃ := inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' h₁ h₂
  simp only [Subtype.coe_eta, Equiv.symm_apply_apply] at h₃
  rw [Multiset.mem_toFinset, Polynomial.mem_normalizedFactors_iff
    (map_monic_ne_zero (minpoly.monic ζ.isIntegral))] at h₂
  have : P.IsMaximal := .of_liesOver_isMaximal P 𝒑
  rw [h₃, natDegree_of_dvd_cyclotomic_of_irreducible (by simp) hm (f := 1) _ h₂.1]
  · simpa using (orderOf_injective _ Units.coeHom_injective (ZMod.unitOfCoprime p hm)).symm
  · refine dvd_trans h₂.2.2 ?_
    rw [← map_cyclotomic_int, cyclotomic_eq_minpoly (zeta_spec m ℚ K) (NeZero.pos _),
      ← (zeta_spec m ℚ K).coe_toInteger, ← RingOfIntegers.minpoly_coe ζ]
    simp [ζ]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ ((fun s ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s) ∘ Nat.cast) n =
    (∑ k ∈ Finset.Icc 1 n, ↑(Nat.card { I // absNorm I = k })) / ↑n

Tactic:
simp only [Function.comp_apply, Nat.cast_le, ← Nat.cast_sum]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ ↑(Nat.card { I // absNorm ↑I ≤ n }) / ↑n = ↑(∑ x ∈ Finset.Icc 1 n, Nat.card { I // absNorm I = x }) / ↑n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ 𝒑.ramificationIdxIn (𝓞 K) = 1

Tactic:
by
  have : IsGalois ℚ K := isGalois {m} ℚ K
  obtain ⟨⟨P, _, _⟩⟩ := 𝒑.nonempty_primesOver (S := 𝓞 K)
  rw [ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ), ramificationIdx_eq_of_not_dvd p K P hm]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
⊢ ∃ σ, 1 ≤ ‖σ α‖

Tactic:
apply exists_conjugate_one_le_norm (K := K) (α := ⟨α, hα⟩)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
⊢ ⟨α, hα⟩ ≠ 0