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

Goal state before:
pp: this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ

Tactic:
rcases eq_or_ne x 1 with rfl | hx

Goal state after:
case inl
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
⊢ riemannZetaZerosᶜ ∈ nhdsWithin 1 {1}ᶜ

case inr
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
hx : x ≠ 1
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ π ^ 4 / 90 = (-1) ^ 3 * 2 ^ 3 * π ^ 4 * ↑(bernoulli' 4) / ↑4!

pp: ⊢ 4 ≠ 1

Tactic:
bernoulli'_four

Goal state after:
⊢ π ^ 4 / 90 = (-1) ^ 3 * 2 ^ 3 * π ^ 4 * ↑(-1 / 30) / ↑4!

⊢ 4 ≠ 1
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: n q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ IsCoprime ↑a ↑q

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R) →
    Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
rintro ⟨hD, hN, hM⟩
    rw [isNontrivial_iff_nontrivial_units] at hN
    rw [LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
    intro H
    obtain ⟨x, hx, hx'⟩ := hD.has_maximal_element
    obtain ⟨y, hy, hy'⟩ := exists_between hx
    exact hy.not_ge (hx' y hy')

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
⊢ Finite 𝓀[K]

Tactic:
obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]

Goal state after:
case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
⊢ Finite 𝓀[K]
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x : ↥𝒪[K]
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t

Tactic:
replace ht' := ht'.ge (Set.mem_univ x)

Goal state after:
case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x : ↥𝒪[K]
ht' : x ∈ ⋃ y ∈ t, Metric.ball y ‖p‖
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε

Tactic:
obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]

Goal state after:
case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr.e_a.succ
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ (e + 1) * a'
⊢ χ₈ ↑b ^ (e + 1) = χ₈ ↑(b % (4 * a)) ^ (e + 1)

Tactic:
rw [χ₈_nat_mod_eight, χ₈_nat_mod_eight (b % (4 * a)), mod_mod_of_dvd b]

Goal state after:
case inr.e_a.succ
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ (e + 1) * a'
⊢ 8 ∣ 4 * a
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s

Tactic:
obtain hr1 | hr1 := lt_or_ge r 1

Goal state after:
case inl
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
hr1 : r < 1
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s

case inr
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
hr1 : 1 ≤ r
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x : X q
⊢ 1 * x = x

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x : X q
⊢ x * 1 = x

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ↑0 = 0

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ (↑↑n, 0) = ↑n

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ (↑(Int.negSucc n), 0) = -↑(n + 1)

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝ : X q
⊢ 0 * x✝ = 0

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝ : X q
⊢ x✝ * 0 = 0

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
n m : ℤ
⊢ ↑(n * m) = ↑n * ↑m

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this✝ : NeZero n
this : ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1
⊢ ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) (primitiveRoots n ℂ).val, x = 1

Tactic:
by simpa

Goal state after:
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 ?m.84)

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
this : DiscreteTopology ↥(zpowers g⁻¹)
ha : ¬1 ≤ g
⊢ DiscreteTopology ↥(zpowers g)

Tactic:
rwa [zpowers_inv] at this

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

Goal state before:
pp: N✝ N : ℕ
⊢ ∀ (x y : ↥(Gamma0 N)), ↑(↑↑(x * y) 1 1) = ↑(↑↑x 1 1) * ↑(↑↑y 1 1)

Tactic:
by
    rintro ⟨A, hA⟩ ⟨B, _⟩
    simp only [MulMemClass.mk_mul_mk, Fin.isValue, coe_mul, (two_mul_expl A.1 B).2.2.2,
      Int.cast_add, Int.cast_mul, Gamma0_mem.mp hA, zero_mul, zero_add]

Goal state after:
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
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
c : K
hc : ¬↑g 1 0 = 0
⊢ discrim (↑g 1 0) (↑g 1 1 - ↑g 0 0) (-↑g 0 1) = 0

Tactic:
rw [discrim]

Goal state after:
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
c : K
hc : ¬↑g 1 0 = 0
⊢ (↑g 1 1 - ↑g 0 0) ^ 2 - 4 * ↑g 1 0 * -↑g 0 1 = 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: a : SL(2, ℤ)
this : ((mapGL ℝ) ModularGroup.T).IsParabolic
⊢ ((mapGL ℝ) (a * ModularGroup.T * a⁻¹)).IsParabolic

Tactic:
by simpa

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

Goal state before:
pp: case mp
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • ∞ = (mapGL ℝ) g • ∞

Tactic:
← (Rat.castHom ℝ).algebraMap_toAlgebra,

Goal state after:
case mp
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (algebraMap ℚ ℝ)) ((mapGL ℚ) g) • ∞ = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • ∞ = (mapGL ℝ) g • ∞

Tactic:
← (Rat.castHom ℝ).algebraMap_toAlgebra,

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (algebraMap ℚ ℝ)) ((mapGL ℚ) g) • ∞ = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g⁻¹) • ∞ = (mapGL ℝ) g⁻¹ • ∞

Tactic:
← (Rat.castHom ℝ).algebraMap_toAlgebra,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (algebraMap ℚ ℝ)) ((mapGL ℚ) g⁻¹) • ∞ = (mapGL ℝ) g⁻¹ • ∞
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
this : GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ
⊢ f (h +ᵥ τ) = (⇑f ∣[k] GeneralLinearGroup.upperRightHom h) τ

Tactic:
by
    simp_rw [slash_def, this]
    simp [σ, denom, GeneralLinearGroup.val_det_apply, denom]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
hG : DiscreteTopology ↥𝒢
H : Set (GL (Fin 2) R) := ↑𝒢 ∩ Set.range ⇑upperRightHom
hH : DiscreteTopology ↑H
x : R
hx : x ∈ ↑𝒢.strictPeriods
⊢ upperRightHom x ∈ H

Tactic:
grind [SetLike.mem_coe, Subgroup.mem_strictPeriods_iff]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
⊢ f.ker = ⊥

Tactic:
suffices ((z : ℂ).im⁻¹ • g).comp f = LinearMap.id by exact LinearMap.ker_eq_bot_of_inverse this

Goal state after:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
⊢ ((↑z).im⁻¹ • g) ∘ₗ f = LinearMap.id
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_4
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
hf : f.ker = ⊥
hf' : IsClosedEmbedding ⇑f
⊢ cofinite = Filter.coprodᵢ fun x ↦ cofinite

Tactic:
rw [coprodᵢ_cofinite]

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

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖qExpansionFormalMultilinearSeries h f n‖ * ↑r ^ n

Tactic:
simp only [qExpansionFormalMultilinearSeries_apply_norm]

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖(PowerSeries.coeff n) (qExpansion h ⇑f)‖ * ↑r ^ n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ ρ ∈ 𝒟

Tactic:
by
  constructor <;> norm_num [ρ, ← pow_two, div_pow]

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

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r a)
⊢ (fun v ↦ ⟨↑v ᵥ* ↑γ⁻¹, ⋯⟩) ((fun v ↦ ⟨↑v ᵥ* ↑γ, ⋯⟩) v) = v

Tactic:
simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]

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

Goal state before:
pp: h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun x ↦ 2 * ↑π * I / ↑h * x
⊢ logDeriv (𝕢 h) z = 2 * ↑π * I / ↑h

Tactic:
rw [this, logDeriv_comp (by fun_prop) (by fun_prop), deriv_const_mul_id]

Goal state after:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun x ↦ 2 * ↑π * I / ↑h * x
⊢ logDeriv cexp (2 * ↑π * I / ↑h * z) * (2 * ↑π * I / ↑h) = 2 * ↑π * I / ↑h
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case pos
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

pp: case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
· by_cases hn : n = -1
      · simp [hb, hn, δ_eq_two]
        ring
      · have hn0 : (n : ℂ) ≠ 0 := by aesop
        have hn1 : (n : ℂ) + 1 ≠ 0 := by norm_cast; grind
        simp [δ, h, hb, hn]
        grind

Goal state after:
case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hf
htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1))) ^ 24) atImInfty (𝓝 1)
τ : ℍ
⊢ Multipliable fun n ↦ 1 - cexp (2 * ↑π * I * ↑τ) ^ (n + 1)

Tactic:
apply (multipliableLocallyUniformlyOn_eta.multipliable τ.2).congr

Goal state after:
case hf
htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1))) ^ 24) atImInfty (𝓝 1)
τ : ℍ
⊢ ∀ (b : ℕ), 1 - eta_q b ↑τ = 1 - cexp (2 * ↑π * I * ↑τ) ^ (b + 1)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1 + Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)

Tactic:
suffices Module.rank ℂ (ModularForm 𝒮ℒ k ⧸ cuspFormSubmodule 𝒮ℒ k) = 1 by
    rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Module.rank ℂ
      (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        (g • z).im = z.im →
          0 ≤ ↑g 1 0 →
            (g = 1 ∨ g = -1) ∨
              (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
                (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
                  (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
                    (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
                      (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                        (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                          (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                            (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ ↑g 1 0
⊢ (-g • z).im = z.im

Tactic:
simpa using him

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
⊢ ∀ (b : ℤ), cexp (↑π * I * ↑b ^ 2 * τ) = jacobiTheta₂_term b 0 τ

Tactic:
by simp [jacobiTheta₂_term]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
have := this.nat_add_neg

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑↑n ^ 2 * τ) + cexp (↑π * I * ↑(-↑n) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ 0 < (I * ↑t⁻¹).im

Tactic:
by simpa

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ 0 < (I * ↑t).im

Tactic:
by simpa

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
simp only [Nat.succ_eq_add_one] at h

Goal state after:
case succ
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
⊢ emultiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
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.succ
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)

Tactic:
simp only [Nat.succ_eq_add_one] at h

Goal state after:
case succ
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)
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) = |∏ w, (x.2 w).1| • f (↑(polarCoordReal K).symm x)

Tactic:
Finset.abs_prod,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) = (∏ x_1, |(x.2 x_1).1|) • f (↑(polarCoordReal K).symm x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ENNReal.ofReal |∏ w, (x.2 w).1| * f (↑(polarCoordReal K).symm x)

Tactic:
Finset.abs_prod,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ENNReal.ofReal (∏ x_1, |(x.2 x_1).1|) * f (↑(polarCoordReal K).symm x)
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inl
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.IsReal
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
have := LiesOver.extensionEmbedding_liesOver_of_isReal w hv
    rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal hv) (ringEquivRealOfIsReal
        (h.liesOver_isReal_over _ _ hv)) (RingHom.ext fun _ ↦ Complex.ofReal_inj.1 <| by simp),
      Module.finrank_self]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ Codisjoint (comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ)) (span {↑p})

Tactic:
rw [codisjoint_comm, ← IsCoatom.not_le_iff_codisjoint, ← under_def, ← Ideal.dvd_iff_le,
    ← Int.ideal_span_absNorm_eq_self (under ℤ (conductor ℤ θ)),
    Ideal.span_singleton_dvd_span_singleton_iff_dvd, Int.natCast_dvd_natCast, exponent]
  exact isMaximal_def.mp <| Int.ideal_span_isMaximal_of_prime p

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
⊢ ↑expMapBasis x = Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
simp_rw [expMapBasis_apply, Basis.equivFun_symm_apply, Fintype.sum_eq_add_sum_subtype_ne _ w₀,
    expMap_add, expMap_smul, expMap_basis_of_eq, Pi.pow_def, Real.exp_one_rpow, Pi.mul_def,
    expMap_sum, expMap_smul, expMap_basis_of_ne, Pi.smul_def, smul_eq_mul, prod_apply, Pi.pow_apply,
    normAtAllPlaces_mixedEmbedding]

Goal state after: