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

Goal state before:
pp: n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
⊢ n.GrahamConjecture f

Tactic:
rintro hn hf

Goal state after:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
⊢ ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : 3 ^ k = -1
⊢ 1 ^ (2 * k + 1) + α ^ (2 * k + 1) = 1 - α

Tactic:
α_pow,

Goal state after:
k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : 3 ^ k = -1
⊢ 1 ^ (2 * k + 1) + 3 ^ k * α = 1 - α
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : H.FiniteIndex
⊢ DiscreteTopology ↥H ↔ DiscreteTopology G

Tactic:
refine ⟨fun hH ↦ ?_, fun hG ↦ inferInstance⟩

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : H.FiniteIndex
hH : DiscreteTopology ↥H
⊢ DiscreteTopology G
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
R : Type u_2
inst✝² : CommRing R
Γ : Subgroup (GL n R)
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
⊢ Γ.HasDetPlusMinusOne ↔ ∀ {g : GL n R}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1

Tactic:
refine ⟨fun h {g} hg ↦ h.abs_det hg, fun h ↦ ⟨?_⟩⟩

Goal state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
R : Type u_2
inst✝² : CommRing R
Γ : Subgroup (GL n R)
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
h : ∀ {g : GL n R}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1
⊢ ∀ {g : GL n R}, g ∈ Γ → GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁶ : CommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedMonoid G
inst✝³ : TopologicalSpace G
inst✝² : OrderTopology G
inst✝¹ : MulArchimedean G
inst✝ : DiscreteTopology G
⊢ IsCyclic G

Tactic:
nontriviality G

Goal state after:
G : Type u_1
inst✝⁶ : CommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedMonoid G
inst✝³ : TopologicalSpace G
inst✝² : OrderTopology G
inst✝¹ : MulArchimedean G
inst✝ : DiscreteTopology G
a✝ : Nontrivial G
⊢ IsCyclic G
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case mp
Γ : Subgroup SL(2, ℤ)
x✝ : (map (mapGL ℝ) Γ).IsArithmetic
h : (map (mapGL ℝ) Γ).Commensurable (mapGL ℝ).range
⊢ Γ.index ≠ 0

Tactic:
simpa [Commensurable, MonoidHom.range_eq_map, ← relIndex_comap,
      comap_map_eq_self_of_injective mapGL_injective] using h

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

Goal state before:
pp: case mpr
Γ : Subgroup SL(2, ℤ)
x✝ : Γ.FiniteIndex
h : Γ.index ≠ 0
⊢ (map (mapGL ℝ) Γ).Commensurable (mapGL ℝ).range

Tactic:
simpa [Commensurable, MonoidHom.range_eq_map, ← relIndex_comap,
      comap_map_eq_self_of_injective mapGL_injective] using h

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

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

Tactic:
simp [h, div_eq_inv_mul, smul_infty_def]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

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

Tactic:
simp [h, div_eq_inv_mul, smul_infty_def]

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
⊢ Function.const ℍ x ∣[0] g = Function.const ℍ x

Tactic:
ext; simp [slash_def, σ, Subgroup.HasDetOne.det_eq hg]

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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖petersson k (⇑f ∣[k] g) (⇑f' ∣[k] g) τ‖

Tactic:
petersson_slash,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 2) * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_3
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this
ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re
e_1✝ : ↑((fun g ↦ ↑g 1) ⁻¹' {p}) = { g // ↑g 1 = p }
g : ↑((fun g ↦ ↑g 1) ⁻¹' {p})
⊢ (↑g • z).re =
    (lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re

Tactic:
exact mod_cast congr_arg Complex.re (smul_eq_lcRow0_add z hp g.2)

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

Goal state before:
pp: 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 (g • τ)‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t

Tactic:
rw [hf_inv g τ] at hF𝒟

Goal state after:
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 • τ ∈ 𝒟
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| ∫ (θ : ℝ) in 0..h * (2 * π / h),
    deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1))

Tactic:
2

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ eisensteinSeries a k (γ • z) =
    eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k z *
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k

Tactic:
eisensteinSeries,

Goal state after:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ ∑' (x : ↑(gammaSet N 1 a)), eisSummand k (↑x) (γ • z) =
    (∑' (x : ↑(gammaSet N 1 (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))), eisSummand k (↑x) z) *
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖ = max 1 (1 / τ.im ^ ↑k) ^ 2

Tactic:
generalize h : τ.im = t

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : ℝ
h : τ.im = t
⊢ max t (1 / t) ^ ↑k / ‖↑t ^ ↑k‖ = max 1 (1 / t ^ ↑k) ^ 2
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ∑ i ∈ (↑b).divisorsAntidiagonal.attach, ‖↑(↑i).2‖ ^ k * ‖r‖ ^ ((↑i).1 * (↑i).2) ≤
    ∑ x ∈ (↑b).divisors, ‖↑↑b‖ ^ k * ‖r ^ ↑b‖

Tactic:
(b : ℕ).divisorsAntidiagonal.sum_attach (fun x ↦ ‖(x.2 : 𝕜)‖ ^ _ * _ ^ (x.1 * x.2)),

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ∑ x ∈ (↑b).divisorsAntidiagonal, ‖↑x.2‖ ^ k * ‖r‖ ^ (x.1 * x.2) ≤ ∑ x ∈ (↑b).divisors, ‖↑↑b‖ ^ k * ‖r ^ ↑b‖
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 = !![1, ↑g 0 0; 0, 1] * ↑S * ↑T

Tactic:
coe_S,

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 = !![1, ↑g 0 0; 0, 1] * !![0, -1; 1, 0] * ↑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 = !![1, ↑g 0 0; 0, 1] * ↑S * ↑T⁻¹

Tactic:
coe_S,

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 = !![1, ↑g 0 0; 0, 1] * !![0, -1; 1, 0] * ↑T⁻¹
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 +ᵥ ρ
⊢ T ^ ↑g 0 0 * S * T⁻¹ = S * T⁻¹ ∨ T ^ ↑g 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

Tactic:
suffices g 0 0 = 0 ∨ g 0 0 = -1 by rcases this with h | h <;> simp [h]

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 +ᵥ ρ
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = -1
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Tendsto (fun z ↦ 𝕢 1 ↑z * ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24) atImInfty (𝓝 (0 * 1))

Tactic:
exact (qParam_tendsto_atImInfty zero_lt_one).mul
    (tendsto_atImInfty_tprod_one_sub_eta_q_pow.congr fun z ↦ by congr 1)

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

Goal state before:
pp: hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
τ : ℍ
hτ : dist (∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24) 1 < 1 / 2
⊢ ‖𝕢 1 ↑τ‖ = rexp (-2 * π * τ.im)

Tactic:
simp [Periodic.qParam, Complex.norm_exp]

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

Goal state before:
pp: z : ℂ
hz : z ∈ {z | 0 < z.im}
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [ModularForm.discriminant, ofComplex_apply_of_im_pos hz]

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

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N
⊢ 2 / ↑z *
        (↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N) -
      (-(2 * ↑π) * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N

Tactic:
← tsum_zero_pnat_eq_tsum_nat
      (by simpa using norm_exp_two_pi_I_lt_one ⟨-N / z, im_pnat_div_pos N z⟩)

Goal state after:
z : ℍ
N : ℕ+
h2 :
  ↑π * I -
        2 * ↑π * I *
          (cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ 0 +
            ∑' (n : ℕ+), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ ↑n) -
      ↑z / -↑↑N =
    ↑π * I -
        2 * ↑π * I *
          (cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ 0 +
            ∑' (n : ℕ+), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ ↑n) -
      ↑z / -↑↑N
⊢ 2 / ↑z *
        (↑π * I -
            2 * ↑π * I *
              (cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ 0 +
                ∑' (n : ℕ+), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ ↑n) -
          ↑z / -↑↑N) -
      (-(2 * ↑π) * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (c : (r : ℕ) × ↑(gammaSet 1 r 0)), eisSummand (↑k) (↑c.snd) z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z

Tactic:
eisensteinSeries,

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (c : (r : ℕ) × ↑(gammaSet 1 r 0)), eisSummand (↑k) (↑c.snd) z =
    riemannZeta ↑k * ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
div_mul_comm,

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h ≈ h'
⊢ (⇑f ∣[k] (↑h)⁻¹) τ = (⇑f ∣[k] (↑h')⁻¹) τ

Tactic:
obtain ⟨j, hj, hj'⟩ : ∃ g ∈ 𝒢, h' = h * g := by
      rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hhh'
      exact ⟨h⁻¹ * h', hhh', mod_cast (mul_inv_cancel_left h h').symm⟩

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h ≈ h'
j : GL (Fin 2) ℝ
hj : j ∈ 𝒢
hj' : ↑h' = ↑h * j
⊢ (⇑f ∣[k] (↑h)⁻¹) τ = (⇑f ∣[k] (↑h')⁻¹) τ
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case zero
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
⊢ emultiplicity (↑p) (x ^ 1 - y ^ 1) = emultiplicity (↑p) (x - y)

Tactic:
pow_one,

Goal state after:
case zero
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
⊢ emultiplicity (↑p) (x - y ^ 1) = emultiplicity (↑p) (x - y)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
⊢ emultiplicity (↑p) (x ^ n - y ^ n) = emultiplicity (↑p) (x - y) + emultiplicity p n

Tactic:
rcases n with - | n
  · simp only [emultiplicity_zero, add_top, pow_zero, sub_self]
  have h : FiniteMultiplicity _ _ := Nat.finiteMultiplicity_iff.mpr ⟨hp.ne_one, n.succ_pos⟩
  simp only [Nat.succ_eq_add_one] at h
  rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩
  conv_lhs => rw [hk, pow_mul, pow_mul]
  rw [Nat.prime_iff_prime_int] at hp
  rw [emultiplicity_pow_sub_pow_of_prime hp,
    emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx, h.emultiplicity_eq_multiplicity]
  · rw [← geom_sum₂_mul]
    exact dvd_mul_of_dvd_right hxy
  · exact fun h => hx (hp.dvd_of_dvd_pow h)
  · rw [Int.natCast_dvd_natCast]
    rintro ⟨c, rfl⟩
    refine hpn ⟨c, ?_⟩
    rwa [pow_succ, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
⊢ ∀ᶠ (i : HeightOneSpectrum R) in Filter.cofinite,
    (fun i ↦ { toCompletion := ↑((WithVal.equiv (valuation K i)).symm k) }) i ∈
      (fun v ↦ ↑(adicCompletionIntegers K v)) i

Tactic:
simp only [Filter.eventually_cofinite, SetLike.mem_coe, mem_adicCompletionIntegers R K,
     valuedAdicCompletion_eq_valuation', not_le]
    exact HeightOneSpectrum.Support.finite R k

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_1
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ 2 ^ 1 ∣ x ^ 2 ^ i + y ^ 2 ^ i

Tactic:
pow_one,

Goal state after:
case refine_1
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ 2 ∣ x ^ 2 ^ i + y ^ 2 ^ i
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] (range (structureMap R A cofinite))

Tactic:
range_structureMap

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), ↑f i ∈ A i}
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2

Tactic:
· rw [← even_iff_two_dvd, Int.not_even_iff_odd]
    apply Odd.pow
    simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
this : ↑(FDerivPolarCoordRealSymm K x) = LinearMap.id.prodMap ↑(fderivPiPolarCoordSymm x.2)
⊢ LinearMap.det ↑(fderivPiPolarCoordSymm x.2) = ∏ w, (x.2 w).1

Tactic:
← ContinuousLinearMap.det,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
this : ↑(FDerivPolarCoordRealSymm K x) = LinearMap.id.prodMap ↑(fderivPiPolarCoordSymm x.2)
⊢ (fderivPiPolarCoordSymm x.2).det = ∏ w, (x.2 w).1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(mixedEmbedding.polarCoord K).symm

Tactic:
by
  rw [polarCoord_symm_eq]
  exact (Homeomorph.measurable _).comp (measurable_polarCoordReal_symm K)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
⊢ ∃ u, u • x ∈ fundamentalCone K

Tactic:
by
  classical
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B
  · exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩
  · obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)
    exact ⟨⟨e, by rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
hx : mixedEmbedding.norm x ≠ 0
⊢ ∃ u, u • x ∈ integerSet K

Tactic:
obtain ⟨u, hu⟩ := exists_unit_smul_mem hx

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
hx : mixedEmbedding.norm x ≠ 0
u : (𝓞 K)ˣ
hu : u • x ∈ fundamentalCone K
⊢ ∃ u, u • x ∈ integerSet K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Surjective (integerSetToAssociates K)

Tactic:
rintro ⟨x⟩
  obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integerSet K := by
    refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
    exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)
  refine ⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩,
    Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩
  simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet,
    unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
    Units.mul_inv_cancel_right]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
φ : K →+* ℂ := ⋯
⊢ φ ((complexConj K) ((algebraMap (𝓞 K) K) ↑↑ζ)) = φ ((algebraMap (𝓞 K) K) ↑↑ζ)⁻¹

Tactic:
rw [complexEmbedding_complexConj, ← Units.complexEmbedding_apply,
    Complex.conj_rootsOfUnity (n := torsionOrder K), Units.val_inv_eq_inv_val,
    Units.complexEmbedding_apply, map_inv₀]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ (Units.complexEmbedding φ) ↑ζ ∈ rootsOfUnity (torsionOrder K) ℂ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card (↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} × ↥(Units.torsion K)) = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}

Tactic:
exact Nat.card_congr (integerSetEquivNorm K n).symm

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
x✝ :
  x ∈
    ⇑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}
h₁ :
  x ∈
    ⇑mixedSpaceOfRealSpace ⁻¹'
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : x ∈ {x | ∀ (w : InfinitePlace K), 0 ≤ x w}
h₃ : x ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0}
h₄ : x ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}
⊢ x ∈ normAtAllPlaces '' normLeOne K

Tactic:
· exact ⟨mixedSpaceOfRealSpace x, ⟨⟨h₁, h₃⟩, h₄⟩, normAtAllPlaces_mixedSpaceOfRealSpace h₂⟩

Goal state after: