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

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this✝ : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz)) }
y : ↥K := ⟨z, ⋯⟩
this : ∃ n, ∃ (_ : 0 < n), y ^ n = 1
⊢ ∃ n, 0 < n ∧ z ^ n = 1

Tactic:
obtain ⟨n, hn₀, hn₁⟩ := this

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz)) }
y : ↥K := ⟨z, ⋯⟩
n : ℕ
hn₀ : 0 < n
hn₁ : y ^ n = 1
⊢ ∃ n, 0 < n ∧ z ^ n = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
⊢ Fintype.card (ZMod q) * Fintype.card (ZMod q) = q ^ 2

Tactic:
ZMod.card q,

Goal state after:
q : ℕ
inst✝ : NeZero q
⊢ q * q = q ^ 2
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)

Tactic:
by_cases h : g 1 0 = 0

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ↑g 1 0 = 0
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ¬↑g 1 0 = 0
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case infty
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

Tactic:
by_cases h : g 1 0 = 0

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
h : ↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
h : ¬↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ (ConjAct.toConjAct h • 𝒢).relIndex ℋ ≠ 0

Tactic:
rw [← ℋ.conjAct_pointwise_smul_eq_self (ℋ.le_normalizer hh), 𝒢.relIndex_pointwise_smul]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ 𝒢.relIndex ℋ ≠ 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
⊢ ∀ (γ : SL(2, ℤ)), f ∣[k] γ = f

Tactic:
intro γ
  have h𝒮ℒ : 𝒮ℒ = Subgroup.closure ({↑S, ↑T} : Set (GL (Fin 2) ℝ)) := by
    rw [MonoidHom.range_eq_map, ← SpecialLinearGroup.SL2Z_generators, MonoidHom.map_closure,
      Set.image_pair]
    rfl
  exact (slash_action_generators h𝒮ℒ).mpr (fun g hg ↦ by rcases hg with rfl | rfl <;> assumption)
    _ (MonoidHom.mem_range.mpr ⟨γ, rfl⟩)

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

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k < 0
f : F
⊢ ⇑f = 0

Tactic:
by
  have hf := levelOne_nonpos_wt_const hk.le f
  rcases wt_eq_zero_of_eq_const k hf with rfl | hf₀
  · exact (lt_irrefl _ hk).elim
  · rw [hf, hf₀, const_zero]

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

Goal state before:
pp: N r : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N r) u v
f : Fin 2 → ℤ
hf : f ∈ gammaSet N r u ∧ f ∈ gammaSet N r v
⊢ u = v

Tactic:
exact hf.1.1.symm.trans hf.2.1

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

Goal state before:
pp: r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
i : Fin 2
⊢ ↑r ∣ v i

Tactic:
fin_cases i <;> simp [← hv.2, Int.gcd_dvd_left, Int.gcd_dvd_right]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ¬↑g 1 0 = 0
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ max τ.im (1 / τ.im)

Tactic:
refine le_trans ?_ <| le_max_right _ _
    rw [show 1 / τ.im = τ.im / τ.im ^ 2 by field_simp]
    gcongr
    rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) =
      ((g 1 0) * τ.re + (g 1 1)) ^ 2 + (g 1 0) ^ 2 * τ.im ^ 2 by simp [Complex.normSq_apply]; ring]
    have : (1 : ℝ) ≤ g 1 0 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs hg)
    nlinarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ ∃ g, g • z ∈ 𝒟

Tactic:
by
  -- obtain a g₀ which maximizes im (g • z),
  obtain ⟨g₀, hg₀⟩ := exists_max_im z
  -- then among those, minimize re
  obtain ⟨g, hg, hg'⟩ := exists_row_one_eq_and_min_re z (bottom_row_coprime g₀)
  refine ⟨g, ?_⟩
  -- `g` has same max im property as `g₀`
  have hg₀' : ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im := by
    have hg'' : (g • z).im = (g₀ • z).im := by
      rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]
    simpa only [hg''] using hg₀
  constructor
  · -- Claim: `1 ≤ ⇑norm_sq ↑(g • z)`. If not, then `S•g•z` has larger imaginary part
    contrapose! hg₀'
    refine ⟨S * g, ?_⟩
    rw [mul_smul]
    exact im_lt_im_S_smul hg₀'
  · change |(g • z).re| ≤ 1 / 2
    -- if not, then either `T` or `T'` decrease |Re|.
    rw [abs_le]
    constructor
    · contrapose! hg'
      refine ⟨T * g, (T_mul_apply_one _).symm, ?_⟩
      rw [mul_smul, re_T_smul]
      cases abs_cases ((g • z).re + 1) <;> cases abs_cases (g • z).re <;> linarith
    · contrapose! hg'
      refine ⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, ?_⟩
      rw [mul_smul, re_T_inv_smul]
      cases abs_cases ((g • z).re - 1) <;> cases abs_cases (g • z).re <;> linarith

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

Goal state before:
pp: k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ MDiff ⇑(eisensteinSeriesSIF a k)

Tactic:
intro τ
  suffices DifferentiableAt ℂ (↑ₕeisensteinSeriesSIF a k) τ.1 by
    convert!
      MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
    exact funext fun z ↦ (comp_ofComplex (eisensteinSeriesSIF a k) z).symm
  refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)
  exact (eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
    (Eventually.of_forall fun s ↦ DifferentiableOn.fun_sum
    fun _ _ ↦ eisSummand_extension_differentiableOn _ _) isOpen_upperHalfPlaneSet

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
convert! this using 2

Goal state after:
case e'_1
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ g = T ∨ g = -T ↔ -g = T ∨ -g = -T

case e'_2.e'_1
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ↔ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2

case e'_2.e'_2
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ g = 1 ∨ g = -1 ↔ -g = 1 ∨ -g = -1
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)) =O[atTop] fun n ↦ ↑n ^ e

Tactic:
have : NeZero h := ⟨hh.ne'⟩

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)) =O[atTop] fun n ↦ ↑n ^ e
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
⊢ ∃ c, IsBigOWith c (comap UpperHalfPlane.im (𝓝 0)) ⇑f fun τ ↦ τ.im ^ (-↑k)

Tactic:
← Int.cast_neg,

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
⊢ ∃ c, IsBigOWith c (comap UpperHalfPlane.im (𝓝 0)) ⇑f fun τ ↦ τ.im ^ ↑(-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
x : ℕ
i : ℤ
hi : i ∈ Finset.Ico (-↑x) ↑x
⊢ Summable fun n ↦ 1 / (↑n * ↑z + ↑i) ^ 2

Tactic:
simpa using! linear_left_summable (ne_zero z) i (k := 2) (by norm_num)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (1 +ᵥ ρ) ∈ 𝒟
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
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝² : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this✝¹ : S • ρ = T • ρ
this✝ : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
this : -↑1 ≤ ↑(↑g 0 0) ∧ ↑g 0 0 ≤ 0
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = -1

Tactic:
← Int.cast_neg,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (1 +ᵥ ρ) ∈ 𝒟
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
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝² : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this✝¹ : S • ρ = T • ρ
this✝ : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
this : ↑(-1) ≤ ↑(↑g 0 0) ∧ ↑g 0 0 ≤ 0
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = -1
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
⊢ (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1

Tactic:
rw [← Matrix.GeneralLinearGroup.val_det_apply]

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
⊢ ↑(Matrix.GeneralLinearGroup.det
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))) =
    1
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‖
hr : ‖r‖ < 1
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖(mkOfCompact c) ⟨z, hz⟩‖ ^ n ≤ ‖mkOfCompact c‖ ^ n
⊢ ‖(f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) z‖ ≤
    ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * |r| ^ n

Tactic:
simp only [norm_mkOfCompact, mkOfCompact_apply, ContinuousMap.coe_mk, ← exp_nsmul', Pi.smul_apply,
    iteratedDerivWithin_cexp_aux k n p isOpen_upperHalfPlaneSet (hK hz), smul_eq_mul,
    norm_mul, norm_pow, Complex.norm_div, norm_ofNat, norm_real, Real.norm_eq_abs, norm_I, mul_one,
    norm_natCast, abs_norm, ge_iff_le, r, c] at *

Goal state after:
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‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖cexp (2 * ↑π * I * z / ↑p)‖ ^ n ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
hr : ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ < 1
⊢ ‖f n‖ * ((2 * |π| * ↑n / |p|) ^ k * ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖) ≤
    ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₆) = -504

Tactic:
by
  norm_num [E_qExpansion_coeff _ ⟨3, rfl⟩, show bernoulli 6 = 1 / 42 by decide +kernel]

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

Goal state before:
pp: case hf
z : ℍ
d : ℕ+
⊢ ∀ (b : ℕ+), 1 / (↑↑↑b * ↑z + ↑(-↑↑d)) - 1 / (↑↑↑b * ↑z + ↑↑↑d) = (-↑↑d + ↑↑b * ↑z)⁻¹ - (↑↑d + ↑↑b * ↑z)⁻¹

Tactic:
grind [Int.cast_natCast]

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

Goal state before:
pp: 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)

Tactic:
simp only [← exp_nsmul, nsmul_eq_mul, Nat.cast_mul] at *

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

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

Tactic:
← PNat.tendsto_comp_val_iff

Goal state after:
z : ℍ
⊢ Tendsto (fun x ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑x / ↑z - ↑↑m) + 1 / (-↑↑x / ↑z + ↑↑m))) atTop (𝓝 (-2 * ↑π * I / ↑z))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun x ↦ ‖1 / ↑x ^ k‖

Tactic:
by simp [hk1]

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun x ↦ ‖(↑x ^ k)⁻¹‖

Tactic:
by simp [hk1]

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

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
h2 : k = 2 * (k / 2 - 1 + 1)
⊢ (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! = -(2 * ↑k / ↑(bernoulli k))

Tactic:
set m := k / 2 - 1

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! = -(2 * ↑k / ↑(bernoulli k))
Module: Mathlib.NumberTheory.Modular

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

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

Tactic:
· exact mem_closure_of_one_lt_norm hx hx'

Goal state after:
case inr
x : ℍ
hx✝ : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
hx : 1 = ‖↑x‖
⊢ x ∈ closure 𝒟ᵒ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.re ^ 2 + z.im ^ 2 ≤ (1 / 2) ^ 2 + y ^ 2

Tactic:
apply add_le_add

Goal state after:
case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.re ^ 2 ≤ (1 / 2) ^ 2

case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ^ 2 ≤ y ^ 2
Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K∞
hx : ¬IsUnit x
⊢ ‖x‖ = 0

Tactic:
rw [Pi.isUnit_iff, not_forall] at hx

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K∞
hx : ∃ x_1, ¬IsUnit (x x_1)
⊢ ‖x‖ = 0
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
⊢ ∀ᶠ (i : ι) in 𝓕, (fun i ↦ ↑(x i)⁻¹) i ∈ (fun i ↦ ↑(B i)) i

Tactic:
by filter_upwards [hx] using fun i hi ↦ hi.2

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬(x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)) % 4 = 0

Tactic:
Int.add_emod,

Goal state after:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬(x ^ 2 ^ (i + 1) % 4 + y ^ 2 ^ (i + 1) % 4) % 4 = 0
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n

pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ n ≠ 0

pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x + (y + 1) ≠ 0

pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 0

Tactic:
· exact Nat.emultiplicity_pow_add_pow hp.out hp1 hxy hx hn

Goal state after:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ n ≠ 0

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x + (y + 1) ≠ 0

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ Submodule.span ℤ (Set.range ⇑B)

Tactic:
Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ unitLattice K
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h₁ : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h₂ : (unitsMulComplexConjInv K).range.index = 2
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
· exact Or.inl <| by rwa [h₂, Nat.mul_eq_right two_ne_zero] at h₁

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace
      (↑expMap.symm
        (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, ?hnc⟩))))))
      x✝ =
    logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))) x✝

pp: case hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ ¬↑i = w₀

Tactic:
realSpaceToLogSpace_expMap_symm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, ?hnc⟩)))) x✝ =
    logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))) x✝

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ (algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, ?hnc⟩)) ≠ 0

case hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ ¬↑i = w₀
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ (completeBasis K) w i = ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))

Tactic:
simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]

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
⊢ (∀ (i : Fin (rank K)),
      ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
            (logMap (mixedSpaceOfRealSpace (↑expMapBasis x))))
          i ∈
        Set.Ico 0 1) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → x w ∈ Set.Ico 0 1

Tactic:
equivFinRank.forall_congr_left,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∀ (b : { w // w ≠ w₀ }),
      ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
            (logMap (mixedSpaceOfRealSpace (↑expMapBasis x))))
          (equivFinRank.symm b) ∈
        Set.Ico 0 1) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1,
          x ↑x_1 •
            (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
              ↑(↑i).mult *
                Real.log
                  (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1))))
                    ↑i))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
normAtAllPlaces_mixedEmbedding,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1,
          x ↑x_1 •
            (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
              ↑(↑i).mult * Real.log (↑i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1)))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n i j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
⊢ Associated (ζ ^ j - 1) (ζ ^ i - 1)

Tactic:
by
  suffices ∀ {j}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1) by
    grind [Associated.trans, Associated.symm]
  exact hζ.associated_sub_one_pow_sub_one_of_coprime

Goal state after: