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

Goal state before:
pp: case e'_5
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
t : ℝ
ht : t ∈ Set.Ioi 1
⊢ -s ≠ 0

Tactic:
· exact neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)

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

Goal state before:
pp: p q : ℕ
hp0 : p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p = #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})

Tactic:
by simp [hp0]

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

Goal state before:
pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

Tactic:
· rfl

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : J(a | p) = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y

Tactic:
by
  rw [← legendreSym.to_jacobiSym] at h
  exact legendreSym.prime_dvd_of_eq_neg_one h hxy

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

Goal state before:
pp: case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * y

Tactic:
rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]

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

Goal state before:
pp: case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * x = y

Tactic:
rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]

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

Goal state before:
pp: case inl
b : ℕ
hb : Odd b
⊢ J(↑0 | b) = J(↑0 | b % (4 * 0))

Tactic:
rw [mul_zero, mod_zero]

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

Goal state before:
pp: case inr.inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this✝ : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
this : ∀ (x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), x < y → x ≤ 1 → (Set.Icc x y).Finite
h : 1 < x
⊢ (Set.Icc x y).Finite

Tactic:
specialize this y⁻¹ x⁻¹ (inv_lt_inv' hxy) (inv_le_one_of_one_le (h.trans hxy).le)
      refine (this.inv).subset ?_
      rw [Set.inv_Icc]
      intro
      simp +contextual

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

Goal state before:
pp: case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(a % ↑2 | 2) * J(a | b) = J(a | b)

Tactic:
Nat.cast_ofNat,

Goal state after:
case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(a % 2 | 2) * J(a | b) = J(a | b)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case right
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h✝ : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
m : ℕ
h_m_pos : 0 < m
h_prim : IsPrimitiveRoot z m
⊢ cyclotomic m ℤ ∣ p

Tactic:
rw [cyclotomic_eq_minpoly h_prim h_m_pos]

Goal state after:
case right
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h✝ : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
m : ℕ
h_m_pos : 0 < m
h_prim : IsPrimitiveRoot z m
⊢ minpoly ℤ z ∣ p
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case convert_4
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k ≠ 0

Tactic:
exact zpow_ne_zero k (denom_ne_zero γ z)

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ Function.Surjective (cosetToCuspOrbit 𝒢)

Tactic:
by
  rintro ⟨c, (hc : IsCusp c _)⟩
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'] at hc
  obtain ⟨g, rfl⟩ := hc
  use ⟦g⁻¹⟧
  aesop

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

Goal state before:
pp: case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ (Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)).IsParabolic

Tactic:
rw [GeneralLinearGroup.isParabolic_iff_of_upperTriangular (by simp)]
      simpa using h.ne'

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

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
⊢ IsCusp ∞ 𝒢 → 0 < 𝒢.strictWidthInfty

Tactic:
rintro ⟨g, hgg, hgp, hgi⟩
    apply 𝒢.strictWidthInfty_nonneg.lt_of_ne'
    rw [← AddSubgroup.zmultiples_ne_bot]
    simp only [AddSubgroup.ne_bot_iff_exists_ne_zero, Subtype.exists, Ne, AddSubgroup.mk_eq_zero,
      exists_prop, and_comm, ← strictPeriods_eq_zmultiples_strictWidthInfty, mem_strictPeriods_iff]
    -- We have some `g ∈ 𝒢` which is parabolic and fixes `∞`. So `g = ±[1, x; 0, 1]` some `x ≠ 0`.
    rw [smul_infty_eq_self_iff] at hgi
    rw [Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular hgg hgi] at hgp
    rcases hgp with ⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩
    · -- If `g = [1, x; 0, 1]`, we're done
      exact ⟨x, hx, hgg⟩
    · -- If `g = -[1, x; 0, 1]` then `g ^ 2 = [1, 2 * x; 0, 1]`.
      exact ⟨2 • x, by grind,
        by simpa only [AddChar.map_nsmul_eq_pow, neg_sq] using pow_mem hgg 2⟩

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ 0 < 𝒢.strictWidthInfty

Tactic:
rw [strictWidthInfty_pos_iff]
  simpa [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff]
    using ⟨_, OnePoint.map_infty _⟩

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]
⊢ Tendsto (fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)

Tactic:
have hmB : Continuous mB := by
    refine continuous_matrix ?_
    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:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
⊢ Tendsto (fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_3.«1»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
j : Fin 2
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩) j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
· rfl

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

Goal state before:
pp: case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * (‖f x‖ * x.im ^ k)) =O[atImInfty] fun τ ↦ 1 * Real.exp (-a * τ.im)

Tactic:
have hf' : IsBoundedAtImInfty f' := ModularFormClass.bdd_at_infty f'

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
hf' : IsBoundedAtImInfty ⇑f'
⊢ (fun x ↦ ‖f' x‖ * (‖f x‖ * x.im ^ k)) =O[atImInfty] fun τ ↦ 1 * Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
τ : ℍ
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
hdenom : ‖denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
⊢ ‖f τ‖ ≤ ‖f (γ • τ)‖

Tactic:
simpa only [slash_action_eqn_SL'' _ (mem_Gamma_one γ), norm_mul, norm_zpow]
      using le_mul_of_one_le_left (norm_nonneg _) <|
        one_le_zpow_of_nonpos₀ (norm_pos_iff.2 (denom_ne_zero _ _)) hdenom hk

Goal state after:
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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)

Tactic:
by
  have := ((differentiableOn_cuspFunction_ball hh hfper hfhol hfbdd).mono
    (Metric.closedBall_subset_ball hR')).circleIntegral_one_div_sub_center_pow_smul hR n
  rw [smul_eq_mul, div_eq_mul_inv, mul_assoc, mul_comm, ← div_eq_iff two_pi_I_ne_zero] at this
  simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_mul]

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

Goal state before:
pp: r : ℕ
a : ℤ
v : Fin 2 → ℤ
hv : finGcdMap v = r
⊢ finGcdMap (a • v) = a.natAbs * r

Tactic:
simp [finGcdMap, Int.gcd_mul_left, hv]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:

Tactic:
|(n : ℝ)| ≤ |z.re| + |z.re + (n : ℝ)| := abs_add' (n : ℝ) z.re
    _ < 1 / 2 + 1 / 2 := add_lt_add h₁ h₂
    _ = 1 := add_halves 1

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
hk' : 2 < ↑k
⊢ Summable fun i ↦ r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖i‖ ^ (-k)

Tactic:
exact_mod_cast (summable_one_div_norm_rpow hk').mul_left <| r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k)

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

Goal state before:
pp: z : ℂ
hz : z ∈ ℍₒ
⊢ Summable fun i ↦ logDeriv (fun x ↦ 1 - eta_q i x) z

Tactic:
have := summable_norm_pow_mul_geometric_div_one_sub 1 (norm_qParam_lt_one 1 ⟨z, hz⟩)
  convert! ((summable_nat_add_iff 1).mpr this).mul_left (-2 * π * I) using 1 with n
  grind [one_sub_eta_logDeriv_eq]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inl
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = 1

Tactic:
rcases case_c_one_d_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩

Goal state after:
case inr.inr.inl.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(S * T) 1 0
hc : ↑(S * T) 1 0 = 1
hd : ↑(S * T) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T))) ↑ρ) = 1

case inr.inr.inl.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S * T) 1 0
hc : ↑(T * S * T) 1 0 = 1
hd : ↑(T * S * T) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (T * S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S * T))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S * T))) ↑ρ) = 1
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
⊢ f = 0

Tactic:
induction k using Nat.strong_induction_on with | _ k ih =>
  have h0 : (qExpansion 1 f).coeff 0 = 0 :=
    PowerSeries.coeff_of_lt_order _ ((Nat.cast_nonneg _).trans_lt h)
  suffices CuspForm.discriminantEquiv (toCuspForm f h0) = 0 by
    simpa [CuspForm.discriminantEquiv.map_eq_zero_iff, DFunLike.ext_iff]
  rcases lt_or_ge k 12 with hk12 | hk12
  · apply rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero (by lia))
  · rw [← mcast_eq_zero_iff (b := ↑(k - 12)) (by lia) rfl]
    refine ih (k - 12) (by lia) ?_
    have hsucc : k / 12 = (k - 12) / 12 + 1 := by lia
    rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h
    exact (ENat.add_lt_add_iff_right (ENat.natCast_ne_top 1)).mp h

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
⊢ f (↑ofComplex (I * ↑(1 / t))) =
    (I ^ k * ↑(t ^ ↑k)) •
      (fun τ ↦
          (σ (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
                (f
                  (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
                    τ)) *
              ↑|↑(Matrix.GeneralLinearGroup.det
                        (Matrix.SpecialLinearGroup.toGL
                          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))| ^
                (k - 1) *
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
                ↑τ ^
              (-k))
        (↑ofComplex (I * ↑t))

Tactic:
suffices f (ofComplex (I * t⁻¹)) = I ^ k * t ^ k *
        (f ((ModularGroup.S : GL (Fin 2) ℝ) • ofComplex (I * t)) * ofComplex (I * t) ^ (-k)) by
      simpa [σ, denom]

Goal state after:
Γ : 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
⊢ f (↑ofComplex (I * ↑t⁻¹)) =
    I ^ k * ↑t ^ k *
      (f
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
            ↑ofComplex (I * ↑t)) *
        ↑(↑ofComplex (I * ↑t)) ^ (-k))
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝² : Field K
v : InfinitePlace K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
w : InfinitePlace L
x : WithAbs ↑v
⊢ (algebraMap (WithAbs ↑v) w.Completion) x = { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }

Tactic:
by
  apply ext
  rw [algebraMap_toCompletion]
  exact UniformSpace.Completion.algebraMap_def (WithAbs w.1) (WithAbs v.1) x

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

Goal state before:
pp: case hx
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) x ≠ 0

pp: case hy
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) y ≠ 0

Tactic:
· exact mixedEmbedding.norm_ne_zero_iff.mp hx w

Goal state after:
case hy
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) y ≠ 0
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 →+* ℂ := Classical.choice ⋯
⊢ (complexConj K) ((algebraMap (𝓞 K) K) ↑↑ζ) = ((algebraMap (𝓞 K) K) ↑↑ζ)⁻¹

Tactic:
apply φ.injective

Goal state after:
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) ↑↑ζ)⁻¹
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
x✝ : (𝓞 K)ˣ
⊢ x✝ ∈ (unitsMulComplexConjInv K).ker ↔ x✝ ∈ realUnits K

Tactic:
rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ realUnits K = (unitsMulComplexConjInv K).ker

Tactic:
rw [unitsMulComplexConjInv_ker]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMap.source = Set.univ

Tactic:
expMap,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (OpenPartialHomeomorph.pi fun w ↦ expMap_single w).source = Set.univ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMap.target = Set.univ.pi fun x ↦ Set.Ioi 0

Tactic:
expMap,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (OpenPartialHomeomorph.pi fun w ↦ expMap_single w).target = Set.univ.pi fun x ↦ Set.Ioi 0
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})

Tactic:
exact isMaximal_def.mp <| Int.ideal_span_isMaximal_of_prime p

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
this : CharP K p
⊢ NeZero ↑n

Tactic:
exact ⟨fun h0 ↦ Nat.Prime.not_coprime_iff_dvd.mpr
        ⟨p, hp.out, dvd_pow_self p (f_ne_zero hK), (CharP.cast_eq_zero_iff K p n).mp h0⟩
          (hn.pow_left f)⟩

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 : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩)).ramificationIdx
      ℤ =
    multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
ramificationIdx_eq_multiplicity (span {↑p}) _ (map_ne_bot_of_ne_bot (by simp [NeZero.ne p]))

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ multiplicity (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩))
      (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p})) =
    multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

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

Tactic:
by
  use (hζ.isUnit (by lia)).unit ^ i * (hζ.geom_sum_isUnit hn hjn).unit
  suffices (ζ - 1) * ζ ^ i * ∑ i ∈ range j, ζ ^ i = (ζ ^ (i + j) - ζ ^ i) by
    simp [← this, mul_assoc]
  grind [mul_geom_sum]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI : absNorm I ≠ 1
n : ℕ
ζ : K
hn : 2 ≤ n
hζ : IsPrimitiveRoot ζ n
h : hζ.toInteger - 1 ∈ I
h₁ : (absNorm I).Coprime n
p : ℕ
hp : Nat.Prime p
h₂ : p ∣ absNorm I
⊢ False

Tactic:
have : Fact (p.Prime) := ⟨hp⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI : absNorm I ≠ 1
n : ℕ
ζ : K
hn : 2 ≤ n
hζ : IsPrimitiveRoot ζ n
h : hζ.toInteger - 1 ∈ I
h₁ : (absNorm I).Coprime n
p : ℕ
hp : Nat.Prime p
h₂ : p ∣ absNorm I
this : Fact (Nat.Prime p)
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ ↑p ∈ under ℤ (span {hζ.toInteger - 1})

Tactic:
mem_comap,

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ (algebraMap ℤ (𝓞 K)) ↑p ∈ span {hζ.toInteger - 1}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : ¬w = w₀
⊢ y w = y w

Tactic:
· rfl

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : w = w₀
⊢ 0 ∈ {0}

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1

Tactic:
· rfl

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ compactSet K =ᵐ[volume] ↑expMapBasis '' closure (paramSet K)

Tactic:
rw [compactSet_eq_union]
  exact union_ae_eq_left_of_ae_eq_empty (by simp)

Goal state after: