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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)

Tactic:
have hswap :
    #{x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p} =
      #{x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} :=
    card_equiv (Equiv.prodComm _ _)
      (fun ⟨_, _⟩ => by
        simp +contextual only [mem_filter, Prod.swap_prod_mk,
          mem_product, Equiv.prodComm_apply, and_assoc, and_left_comm])
  have hdisj :
    Disjoint {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q}
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} := by
    apply disjoint_filter.2 fun x hx hpq hqp => ?_
    have hxp : x.1 < p := lt_of_le_of_lt (b := p / 2)
      (by grind) (Nat.div_lt_self hp.1.pos (by decide))
    have : (x.1 : ZMod p) = 0 := by
      simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
    apply_fun ZMod.val at this
    rw [val_cast_of_lt hxp, val_zero] at this
    simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and, mem_product] at hx
  have hunion :
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
        {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
      Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ :=
    Finset.ext fun x => by
      have := le_total (x.2 * p) (x.1 * q)
      simp only [mem_union, mem_filter, mem_Ico, mem_product]
      tauto
  rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_union_of_disjoint hdisj, hunion,
    card_product]
  simp only [card_Ico, succ_sub_succ_eq_sub, Nat.sub_zero]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ J(-1 | n) = χ₄ ↑n

Tactic:
jacobiSym.at_neg_one hn

Goal state after:
case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ χ₄ ↑n = χ₄ ↑n
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
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ y - x ∈ Ideal.span {p}

Tactic:
← SetLike.mem_coe,

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 y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ y - x ∈ ↑(Ideal.span {p})
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
simp only [ha₂, Nat.cast_mul, ← mul_assoc]

Goal state after:
case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ ↑a' ∣ ↑4 * ↑(2 ^ e) * ↑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 : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
x : K
⊢ (valuation K) x ≤ (valuation K) γ ↔
    Valued.v.restrict r / Valued.v.restrict γ * Valued.v.restrict x ≤ (valuation K).restrict r

Tactic:
div_mul_eq_mul_div,

Goal state after:
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 : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
x : K
⊢ (valuation K) x ≤ (valuation K) γ ↔
    Valued.v.restrict r * Valued.v.restrict x / Valued.v.restrict γ ≤ (valuation K).restrict r
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ -legendreSym 3 ↑(mersenne p) = -1

Tactic:
legendreSym.mod

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ -legendreSym 3 (↑(mersenne p) % ↑3) = -1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case mp
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 → sMod p (p - 2) = 0

pp: case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0

Tactic:
· -- We want to use that fact that `0 ≤ s_mod p (p-2) < 2^p - 1`
    -- and `lucas_lehmer_residue p = 0 → 2^p - 1 ∣ s_mod p (p-2)`.
    intro h
    apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _
      (by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h) <;> clear h
    · exact sMod_nonneg _ (by positivity) _
    · exact sMod_lt _ (by positivity) _

Goal state after:
case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
⊢ OnePoint K

Tactic:
refine Projectivization.lift
      (fun u : {v : Fin 2 → K // v ≠ 0} ↦ if u.1 1 = 0 then ∞ else ((u.1 1)⁻¹ * u.1 0)) ?_ p

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
⊢ ∀ (a b : { v // v ≠ 0 }) (t : K),
    ↑a = t • ↑b → (if ↑a 1 = 0 then ∞ else ↑((↑a 1)⁻¹ * ↑a 0)) = if ↑b 1 = 0 then ∞ else ↑((↑b 1)⁻¹ * ↑b 0)
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
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 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint

Tactic:
have : discrim (g 1 0) (g 1 1 - g 0 0) (-g 0 1) = 0 := by rw [discrim]; grind

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

Goal state before:
pp: case coe
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
q : K
⊢ ∃ g, (mapGL K) g • ∞ = ↑q

Tactic:
| coe q =>

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

Goal state before:
pp: k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] A = f ∣[k1] A * g ∣[k2] A

Tactic:
by
  simp [SL_slash, mul_slash]

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

Goal state before:
pp: case empty
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ 1 ∣[0] g = |(↑g).det|⁻¹ • 1

Tactic:
ext _

Goal state after:
case empty
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
x✝ : ℍ
⊢ (1 ∣[0] g) x✝ = (|(↑g).det|⁻¹ • 1) x✝
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
map_mapGL

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
⊢ (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1

Tactic:
ext x
  simp only [mem_strictPeriods_iff, Subgroup.mem_map, Units.ext_iff, mapGL_coe_matrix,
    map_apply_coe]
  refine ⟨fun ⟨g, _, hg⟩ ↦ ⟨g 0 1, by simpa using congr_fun₂ hg 0 1⟩, ?_⟩
  rintro ⟨m, rfl⟩
  refine ⟨ModularGroup.T ^ m, zpow_mem hΓ m, ?_⟩
  ext i j
  fin_cases i <;> fin_cases j <;> simp [ModularGroup.coe_T_zpow]

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : DiscreteTopology ↥𝒢.periods
⊢ 𝒢.IsRegularAtInfty ↔ 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
by
  refine ⟨fun h ↦ h ▸ widthInfty_mem_periods 𝒢, fun h ↦ ?_⟩
  apply 𝒢.strictPeriods_le_periods.antisymm
  rwa [periods_eq_zmultiples_widthInfty, AddSubgroup.zmultiples_le]

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

Goal state before:
pp: case inl
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
hq : ‖0‖ < 1
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
exact hfper.differentiableAt_cuspFunction_zero hh
      (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
        (fun z hz ↦ UpperHalfPlane.mdifferentiableAt_iff.mp (hfhol ⟨z, hz⟩)))
      (hfbdd.comp_tendsto tendsto_comap_im_ofComplex)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ cd]
⊢ ∀ (i j : Fin 2), Continuous fun a ↦ mB a i j

Tactic:
simp only [mB, Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero,
      cons_val_one, and_self_iff]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
refine ⟨g, fun g' => ?_⟩

Goal state after:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ (g' • z).im ≤ (g • z).im
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
⊢ u = v

Tactic:
obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv

Goal state after:
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
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, ℤ)
⊢ Tendsto (fun τ ↦ ‖petersson k (⇑f) (⇑f') (g • τ)‖) atImInfty (𝓝 0)

Tactic:
← tendsto_zero_iff_norm_tendsto_zero

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, ℤ)
⊢ Tendsto (fun τ ↦ petersson k (⇑f) (⇑f') (g • τ)) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: 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)
τ : ℍ
⊢ ∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑τ) ^ (n + 1)) ^ 24 = (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑τ) ^ (n + 1))) ^ 24

Tactic:
Multipliable.tprod_pow

Goal state after:
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 - cexp (2 * ↑π * I * ↑τ) ^ (b + 1))) ^ 24 = (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑τ) ^ (n + 1))) ^ 24

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)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * ∑' (n : ℕ+), ↑↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
by
  rw [EisensteinSeries.qExpansion_identity hk z, ← tsum_zero_pnat_eq_tsum_nat]
  · simp [show k ≠ 0 by grind]
  · apply (summable_pow_mul_cexp k 1 z).congr
    simp

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

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

Tactic:
exact fun i hi ↦ by simpa using! linear_left_summable (ne_zero z) i le_rfl

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝² : T • z ≠ z
this✝¹ : T⁻¹ • z ≠ z
this✝ : ↑z ≠ -↑I
this : S • z ≠ z
⊢ g = 1 ∨ g = -1

Tactic:
all_goals grind [cases_of_mem_fd_smul_mem_fd hz (hg ▸ hz), SL_neg_smul]

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

Goal state before:
pp: τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑(↑2 +ᵥ τ) = 2 + ↑τ

Tactic:
UpperHalfPlane.coe_vadd

Goal state after:
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑↑2 + ↑τ = 2 + ↑τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

Tactic:
pow_succ',

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (fun n ↦ rexp (-π * τ.im) * rexp (-π * τ.im) ^ n) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
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‖ ^ 2 ≤ √((1 / 2) ^ 2 + y ^ 2) ^ 2

Tactic:
Real.sq_sqrt (by positivity),

Goal state after:
case right
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ ‖z‖ ^ 2 ≤ (1 / 2) ^ 2 + y ^ 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✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
c✝ : OnePoint ℝ
h : IsCusp c✝ ℋ
γ : GL (Fin 2) ℝ
⊢ γ • OnePoint.infty = c✝ → IsZeroAtImInfty ((ModularForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
by
    rintro rfl
    simp_rw [ModularForm.toFun_eq_coe, ModularForm.coe_trace, IsZeroAtImInfty, Filter.ZeroAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]
    let := Fintype.ofFinite 𝒬
    rw [show (0 : ℂ) = ∑ c : ℋ ⧸ 𝒢.subgroupOf ℋ, 0 by simp]
    refine tendsto_finsetSum _ (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ ?_)
    refine (translate f _).zero_at_cusps' ?_ γ rfl
    simpa using h.of_isFiniteRelIndex_conj hr

Goal state after:
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝³ : Group Γ
inst✝² : TopologicalSpace α
inst✝¹ : SMul Γ α
inst✝ : ProperlyDiscontinuousSMul Γ α
G : Subgroup Γ
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | (g • K ∩ L).Nonempty}.Finite

Tactic:
exact finite_disjoint_inter_image

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

Goal state before:
pp: case e'_5.inr
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
n : ℕ
hn : n > 0
⊢ (if 2 * ↑n / h Γ = 0 then 0 else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑n / h Γ) * t))) =
    if n = 0 then 0
    else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ n

Tactic:
simp [hn.ne', Function.Periodic.qParam, ofComplex_apply_eq_ite, ht, ← exp_nat_mul]
        grind [I_sq]

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
QU : DFunLike.coe ⁻¹' U ⊆ DFunLike.coe ⁻¹' Q
⊢ IsCompact (DFunLike.coe ⁻¹' Q)

pp: case refine_2
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
QU : DFunLike.coe ⁻¹' U ⊆ DFunLike.coe ⁻¹' Q
⊢ DFunLike.coe ⁻¹' U ∈ 𝓝 x

Tactic:
· refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left

Goal state after:
case refine_2
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
QU : DFunLike.coe ⁻¹' U ⊆ DFunLike.coe ⁻¹' Q
⊢ DFunLike.coe ⁻¹' U ∈ 𝓝 x
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
pow_succ',

Goal state after:
case refine_2.succ
x✝ y : ℤ
hx✝ : ¬2 ∣ x✝
hxy : 4 ∣ x✝ - y
hx_odd : Odd x✝
hxy_even : Even (x✝ - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
⊢ x ^ (2 * 2 ^ i) % 4 = 1
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup =
    AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))

Tactic:
Subgroup.toAddSubgroup_closure,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup =
    AddSubgroup.map (logEmbedding K) (AddSubgroup.closure (⇑Additive.toMul ⁻¹' Set.range u))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
⊢ Continuous[topologicalSpace R₁ A₁ 𝓕₁, topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ)

Tactic:
rw [continuous_dom]
  intro S hS
  set T := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
  have hT : 𝓕₂ ≤ 𝓟 T := by
    rw [le_principal_iff] at hS ⊢
    exact inter_mem (hf hS) hφ
  have hf' : Tendsto f (𝓟 T) (𝓟 S) := by aesop
  have hφ' : ∀ᶠ j in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j) := by aesop
  have key : mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS =
      inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ' := rfl
  rw [key]
  exact continuous_inclusion _ |>.comp <|
    continuous_rng_of_principal.mpr <|
    continuous_pi fun j ↦ φ_cont j |>.comp <| continuous_eval (f j)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑(polarCoordReal K).symm '' (polarCoordReal K).target =ᵐ[volume] Set.univ

Tactic:
by
  rw [← Set.univ_prod_univ, volume_eq_prod, (polarCoordReal K).symm_image_target_eq_source,
    polarCoordReal_source, ← polarCoord.symm_image_target_eq_source, ← Set.piMap_image_univ_pi]
  exact set_prod_ae_eq .rfl pi_polarCoord_symm_target_ae_eq_univ

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
⊢ (algebraMap F K).comp (algebraMap F K).rangeRestrictFieldEquiv.symm.toRingHom =
    (RingEquiv.refl K).toRingHom.comp (algebraMap (↥(algebraMap F K).fieldRange) K)

Tactic:
by ext; simp; rfl

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)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm) Q ∈
    {d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ))}

Tactic:
← primesOverSpanEquivMonicFactorsModAux_symm_apply

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsModAux✝ ?A).symm ⟨Q, ?hQ⟩) ∈
    {d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ))}

case A
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ ℤ[X]

case hQ
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ Q ∈ (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) ?A)).toFinset