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

Goal state before:
pp: case pos
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : ¬Φ 0 = 0
h' : ∑ j, Φ j = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ

Tactic:
simp [U, Uc, h, h', and_comm]

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

Goal state before:
pp: case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : ¬Φ 0 = 0
h' : ¬∑ j, Φ j = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ

Tactic:
simp [U, Uc, h, h', and_comm]

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

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
⊢ Summable F''

Tactic:
refine (Summable.mul_left 2 this).of_nonneg_of_le (fun pk ↦ ?_) (fun pk ↦ F''_le pk.1 pk.2)
    simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]
    positivity [vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
⊢ (fun x ↦ LFunction χ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x ↦ ↑x

Tactic:
by
  simp_rw [add_comm (1 : ℂ), add_assoc]
  have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).hasDerivAt
  rw [← zero_add (1 + _)] at this
  simpa only [zero_add, h, sub_zero]
    using (Complex.isBigO_comp_ofReal_nhds
      (this.comp_add_const 0 _).differentiableAt.isBigO_sub) |>.mono nhdsWithin_le_nhds

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

Goal state before:
pp: f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

Tactic:
by
  ext1 s
  exact LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
    h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false

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

Goal state before:
pp: case succ
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
| succ e ih =>

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤

Tactic:
let f : (I ^ n : Ideal R) →ₗ[R] (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) :=
    Submodule.mkQ _
  let ϖ := h.principal.choose
  have hI : I = Ideal.span {ϖ} := h.principal.choose_spec
  have hϖ : ϖ ^ n ∈ I ^ n := hI ▸ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) n)
  let g : R →ₗ[R] (I ^ n : Ideal R) := (LinearMap.mulRight R ϖ ^ n).codRestrict _ fun x ↦ by
    simp only [LinearMap.pow_mulRight, LinearMap.mulRight_apply]
    -- TODO: change argument of Ideal.pow_mem_of_mem
    exact Ideal.mul_mem_left _ _ hϖ
  have : I = LinearMap.ker (f.comp g) := by
    ext x
    simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
      f, g]
    constructor <;> intro hx
    · exact Submodule.mul_mem_mul hx hϖ
    · rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
      obtain ⟨y, hy⟩ := hx
      rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
      · rw [hI, Ideal.mem_span_singleton]
        exact ⟨y, hy⟩
      · contrapose h'
        rw [hI, h', Ideal.span_singleton_eq_bot]
  let e : (R ⧸ I) ≃ₗ[R] R ⧸ (LinearMap.ker (f.comp g)) :=
    Submodule.quotEquivOfEq I (LinearMap.ker (f ∘ₗ g)) this
  refine e.trans ((f.comp g).quotKerEquivOfSurjective ?_)
  refine (Submodule.mkQ_surjective _).comp ?_
  rintro ⟨x, hx⟩
  rw [hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
  refine hx.imp ?_
  simp [g, LinearMap.codRestrict, eq_comm, mul_comm]

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

Goal state before:
pp: a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯).prod =
    (List.map (⇑χ) (List.map Nat.cast b.primeFactorsList)).prod

Tactic:
List.map_map,

Goal state after:
a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯).prod =
    (List.map (⇑χ ∘ Nat.cast) b.primeFactorsList).prod
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (boxPoly n B₁ B₂).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

Tactic:
trans Set.ncard (α := Fin (n + 1) → ℤ) (Finset.Icc (⌈B₁ ·⌉) (⌊B₂ ·⌋))

Goal state after:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (boxPoly n B₁ B₂).ncard = (↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)).ncard

n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: case calc_2
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ Set.MapsTo (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜) ↑(Ioo 0 n)

Tactic:
simp only [𝒜, forall_mem_diffs, forall_mem_image, mem_Ioo, mem_Iio, Set.MapsTo, mem_coe]

Goal state after:
case calc_2
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ ∀ ⦃x : ℕ⦄,
    x < n →
      ∀ ⦃x_1 : ℕ⦄,
        x_1 < n →
          0 < ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p ∧
            ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p < n
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ x * (y + z) = x * y + x * z

Tactic:
by
  ext <;> dsimp <;> ring

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ (x + y) * z = x * z + y * z

Tactic:
by
  ext <;> dsimp <;> ring

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
⊢ (map (castRingHom ℂ) p).degree ≠ 0

Tactic:
rwa [p.degree_map_eq_of_injective (castRingHom ℂ).injective_int]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
⊢ 2 < q (p' + 2)

Tactic:
refine (minFac_prime (one_lt_mersenne.2 ?_).ne').two_le.lt_of_ne' ?_
  · exact le_add_left _ _
  · rw [Ne, minFac_eq_two_iff, mersenne, Nat.pow_succ']
    exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
N : ℕ
hN : N ≠ 0
h : ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
⊢ ∃ N,
    N ≠ 0 ∧
      toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
refine ⟨N, hN, fun y hy ↦ ?_⟩

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
N : ℕ
hN : N ≠ 0
h : ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
y : GL (Fin 2) ℝ
hy : y ∈ toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N)
⊢ y ∈ Subgroup.map (mapGL ℝ) Γ(M)
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
by
  suffices (ConjAct.toConjAct h • 𝒢).IsFiniteRelIndex ℋ from hc.of_isFiniteRelIndex
  constructor
  rw [← ℋ.conjAct_pointwise_smul_eq_self (ℋ.le_normalizer hh), 𝒢.relIndex_pointwise_smul]
  exact 𝒢.relIndex_ne_zero

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
hg : g • ∞ = c
⊢ IsZeroAtImInfty (f ∣[k] g) → c.IsZeroAt f k

Tactic:
simp [← hg, IsZeroAt.smul_iff, isZeroAt_infty_iff]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_5
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
⊢ cocompact (Fin 2 → ℝ) = Filter.coprodᵢ fun x ↦ cocompact ℝ

Tactic:
· rw [coprodᵢ_cocompact]

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ ‖petersson k (⇑f) (⇑f) τ‖ / (τ.im ^ (↑k / 2)) ^ 2

Tactic:
rw [petersson, ← Real.rpow_mul_natCast τ.im_pos.le]

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ ‖(starRingEnd ℂ) (f τ) * f τ * ↑τ.im ^ k‖ / τ.im ^ (↑k / 2 * ↑2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ 1
hre : (g • z).re = ↑b + z.re
hb : b = 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
left
    rw [hgz, zpow_one, eq_self_iff_true, true_or, true_and]
    rw [hb, Int.cast_one] at hre
    linarith [(le_abs_self _).trans (abs_neg z.re ▸ hz.2), (le_abs_self _).trans hg.2]

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun c ↦ ↑(↑c.snd).2 ^ k * r ^ ((↑c.snd).1 * (↑c.snd).2)

Tactic:
by
  apply Summable.of_norm
  rw [summable_sigma_of_nonneg (fun a ↦ by positivity)]
  constructor
  · exact fun n ↦ (hasSum_fintype _).summable
  · simp only [norm_mul, norm_pow, tsum_fintype, Finset.univ_eq_attach]
    apply Summable.of_nonneg_of_le (f := fun c : ℕ+ ↦ ‖(c : 𝕜) ^ (k + 1) * r ^ (c : ℕ)‖)
      (fun b ↦ Finset.sum_nonneg (fun _ _ ↦ mul_nonneg (by simp) (by simp))) (fun b ↦ ?_)
      (by apply (summable_norm_pow_mul_geometric_of_norm_lt_one (k + 1) hr).subtype)
    transitivity ∑ _ ∈ (b : ℕ).divisors, ‖(b : 𝕜)‖ ^ k * ‖r ^ (b : ℕ)‖
    · rw [(b : ℕ).divisorsAntidiagonal.sum_attach (fun x ↦ ‖(x.2 : 𝕜)‖ ^ _ * _ ^ (x.1 * x.2)),
          sum_divisorsAntidiagonal ((fun x y ↦ ‖(y : 𝕜)‖ ^ k * _ ^ (x * y)))]
      gcongr with i hi
      · simpa using! le_of_dvd b.2 (div_dvd_of_dvd (dvd_of_mem_divisors hi))
      · rw [norm_pow, mul_comm, Nat.div_mul_cancel (dvd_of_mem_divisors hi)]
    · simp only [norm_pow, Finset.sum_const, nsmul_eq_mul, ← mul_assoc, add_comm k 1, pow_add,
        pow_one, norm_mul]
      gcongr
      simpa using! Nat.card_divisors_le_self b

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

Goal state before:
pp: case h.inl
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K = ∅
⊢ HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

pp: case h.inr
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
⊢ HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
· simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn, hN] using tendstoUniformlyOn_empty

Goal state after:
case h.inr
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
⊢ HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: hmem : 0 ∈ Metric.ball 0 1
⊢ derivWithin (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1) 0 = 1

Tactic:
simp [derivWithin_fun_mul differentiableWithinAt_fun_id
          (differentiableOn_tprod_one_sub_pow_pow 24 _ hmem),
          derivWithin_id' _ _ (Metric.isOpen_ball.uniqueDiffWithinAt hmem)]

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

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

Tactic:
(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
this :
  Module.rank ℂ
      (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1 + Module.rank ℂ ↥(cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ
⊢ ∑ x ∈ Ico (-↑N) ↑N, (↑z ^ 2)⁻¹ * ∑' (n : ℤ), ((-(↑x * (↑z)⁻¹) + ↑n) ^ 2)⁻¹ =
    ∑' (n : ℤ), ∑ x ∈ Ico (-↑N) ↑N, ((↑n * ↑z + ↑x) ^ 2)⁻¹

Tactic:
rw [Summable.tsum_finsetSum (fun i hi ↦ linear_left_summable (ne_zero z) i le_rfl)]

Goal state after:
z : ℍ
N : ℕ
⊢ ∑ x ∈ Ico (-↑N) ↑N, (↑z ^ 2)⁻¹ * ∑' (n : ℤ), ((-(↑x * (↑z)⁻¹) + ↑n) ^ 2)⁻¹ =
    ∑ i ∈ Ico (-↑N) ↑N, ∑' (b : ℤ), ((↑b * ↑z + ↑i) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

Tactic:
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.EisensteinSeries.E2.Summable

Goal state before:
pp: case hf
z : ℍ
d : ℕ+
this : Summable fun n ↦ (-↑↑d / ↑z - ↑n)⁻¹ + (-↑↑d / ↑z + ↑n)⁻¹
⊢ Summable fun m ↦ (-↑↑d / ↑z - ↑↑m)⁻¹ + (-↑↑d / ↑z + ↑↑m)⁻¹

Tactic:
apply this.subtype

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤

Tactic:
exact (Complex.subfield_eq_of_closed <| isClosed_image_extensionEmbedding v).resolve_left <|
    subfield_ne_real_of_isComplex hv

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst✝⁵ : (i : ι₁) → SetLike (S₁ i) (R₁ i)
inst✝⁴ : (j : ι₂) → SetLike (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst✝³ : (i : ι₁) → Monoid (R₁ i)
inst✝² : (i : ι₂) → Monoid (R₂ i)
inst✝¹ : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)
inst✝ : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)
φ : (j : ι₂) → R₁ (f j) →* R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)
⊢ mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ 1 = 1

Tactic:
by
    ext i
    exact map_one (φ i)

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
refine emultiplicity_eq_coe.mpr ⟨?_, ?_⟩

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 ^ 1 ∣ x ^ 2 ^ i + y ^ 2 ^ i

case refine_2
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 + 1) ∣ x ^ 2 ^ i + y ^ 2 ^ i
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case zero
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (x ^ 0 - y ^ 0) = emultiplicity 2 (x - y) + emultiplicity 2 ↑0

Tactic:
simp only [pow_zero, sub_self, emultiplicity_zero, Int.ofNat_zero, add_top]

Goal state after:
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) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ∫⁻ (x : realMixedSpace K) in ↑(polarCoordReal K).symm '' (polarCoordReal K).target, f x

Tactic:
lintegral_image_eq_lintegral_abs_det_fderiv_mul volume
      (polarCoordReal K).open_target.measurableSet
      (fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt)
      (polarCoordReal K).symm.injOn f

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| * f (↑(polarCoordReal K).symm x)
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:
MonoidHom.mem_ker,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ : (𝓞 K)ˣ
⊢ (unitsMulComplexConjInv K) x✝ = 1 ↔ x✝ ∈ realUnits K
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ (W.comap (algebraMap (↥L) K)).IsReal

Tactic:
← mk_embedding W,

Goal state after:
K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ ((InfinitePlace.mk W.embedding).comap (algebraMap (↥L) K)).IsReal
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ logMap (mixedSpaceOfRealSpace (↑expMapBasis x)) ∈
      ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → x w ∈ Set.Ico 0 1

Tactic:
ZSpan.mem_fundamentalDomain,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∀ (i : Fin (rank K)),
      ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
            (logMap (mixedSpaceOfRealSpace (↑expMapBasis x))))
          i ∈
        Set.Ico 0 1) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → x w ∈ Set.Ico 0 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: case refine_1
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)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ ↑(frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) ^ orderOf (unitOfCoprime (p ^ f) ⋯)) pB.gen = ↑1 pB.gen

Tactic:
simp only [AlgEquiv.coe_toAlgHom, AlgEquiv.coe_pow, AlgEquiv.one_apply,
      coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, hK]
    nth_rewrite 2 [← pow_one pB.gen]
    rw [powerBasis_gen hPirr.ne_zero, hζ'.pow_eq_pow_iff_modEq, ← hζ.eq_orderOf,
      ← natCast_eq_natCast_iff]
    simpa only [Nat.cast_pow, Nat.cast_one, coe_unitOfCoprime, Units.val_one,
      Units.val_pow_eq_pow_val] using! Units.val_inj.mpr <| pow_orderOf_eq_one
      (unitOfCoprime _ (hn.pow_left f))

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 : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this✝ : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero ↑n
hP : P ∈ normalizedFactors (cyclotomic n K)
⊢ P * P ∣ cyclotomic n K

Tactic:
have : {P, P} ≤ normalizedFactors (cyclotomic n K) := by
    refine le_iff_count.mpr (fun Q ↦ ?_)
    by_cases hQ : Q = P
    · simp only [hQ, insert_eq_cons, count_cons_self, nodup_singleton, mem_singleton,
        count_eq_one_of_mem, reduceAdd]
      lia
    · simp [hQ]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this✝¹ : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this✝ : NeZero ↑n
hP : P ∈ normalizedFactors (cyclotomic n K)
this : {P, P} ≤ normalizedFactors (cyclotomic n K)
⊢ P * P ∣ cyclotomic n K