mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
⊢ ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i

Tactic:
have hj := ht (hc.trans_le hi1)

Goal state after:
case inr.refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
hj : c ∈ ⋃ i ∈ t, U i
⊢ ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
m n : ℕ
h : m < n
⊢ 1 < 2

Tactic:
norm_num1

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
suffices Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s - s * l) (𝓝[>] 1) (𝓝 0) by
    rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
    have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
      tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
    exact (this.add h₃).congr fun _ ↦ by ring

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s - ↑s * l) (𝓝[>] 1) (𝓝 0)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ω * ωb = 1

Tactic:
dsimp [ω, ωb]

Goal state after:
q : ℕ
⊢ (2, 1) * (2, -1) = 1
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
rw [this, one_add_α_pow_q_succ odd leg3]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q✝ i b q k : ℕ
⊢ sModNatTR.go q k b = sModNatAux b q k

Tactic:
induction k generalizing b with
    | zero => rfl
    | succ k ih =>
      rw [sModNatTR.go, ih, sModNatAux]
      clear ih
      induction k with
      | zero => rfl
      | succ k ih =>
        rw [sModNatAux, ih, sModNatAux]

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

Goal state before:
pp: n : Type u_1
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
R : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
inst✝¹ : T2Space R
𝒢 : Subgroup (GL n R)
inst✝ : DiscreteTopology ↥𝒢
⊢ DiscreteTopology ↥𝒢.adjoinNegOne

Tactic:
by
  rwa [𝒢.commensurable_adjoinNegOne_self.discreteTopology_iff]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
this : Γ(N) ≤ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)
x✝ : NeZero N
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0

Tactic:
simpa only [index_comap] using! (finiteIndex_of_le this).index_ne_zero

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

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
⊢ IsCusp (g • c) (ConjAct.toConjAct g • 𝒢)

Tactic:
obtain ⟨p, hp𝒢, hpp, hpc⟩ := hc
  refine ⟨_, 𝒢.smul_mem_pointwise_smul _ _ hp𝒢, ?_, ?_⟩
  · simpa [ConjAct.toConjAct_smul] using hpp
  · simp [ConjAct.toConjAct_smul, mul_smul, hpc]

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

Goal state before:
pp: case zero
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ ⟨0 • k, GradedMonoid.GMonoid.gnpow 0 f⟩ = ⟨↑0 * k, f.pow 0⟩

Tactic:
refine (GradedMonoid.GMonoid.gnpow_zero' ⟨k, f⟩).trans ?_

Goal state after:
case zero
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ 1 = ⟨↑0 * k, f.pow 0⟩
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
obtain ⟨E, hE⟩ : ∃ E, ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / (im τ) ^ t ≤ E := by
    simpa [norm_mul, norm_norm, Real.norm_rpow_of_nonneg (_ : ℍ).im_pos.le,
      Real.norm_of_nonneg (_ : ℍ).im_pos.le]
      using (isCompact_truncatedFundamentalDomain y).exists_bound_of_continuousOn hfm

Goal state after:
E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
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
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
⊢ 2 ≠ 1

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ ∃ g, g • z ∈ 𝒟

Tactic:
obtain ⟨g₀, hg₀⟩ := exists_max_im z
  -- then among those, minimize re
  obtain ⟨g, hg, hg'⟩ := exists_row_one_eq_and_min_re z (bottom_row_coprime g₀)
  refine ⟨g, ?_⟩
  -- `g` has same max im property as `g₀`
  have hg₀' : ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im := by
    have hg'' : (g • z).im = (g₀ • z).im := by
      rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]
    simpa only [hg''] using hg₀
  constructor
  · -- Claim: `1 ≤ ⇑norm_sq ↑(g • z)`. If not, then `S•g•z` has larger imaginary part
    contrapose! hg₀'
    refine ⟨S * g, ?_⟩
    rw [mul_smul]
    exact im_lt_im_S_smul hg₀'
  · change |(g • z).re| ≤ 1 / 2
    -- if not, then either `T` or `T'` decrease |Re|.
    rw [abs_le]
    constructor
    · contrapose! hg'
      refine ⟨T * g, (T_mul_apply_one _).symm, ?_⟩
      rw [mul_smul, re_T_smul]
      cases abs_cases ((g • z).re + 1) <;> cases abs_cases (g • z).re <;> linarith
    · contrapose! hg'
      refine ⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, ?_⟩
      rw [mul_smul, re_T_inv_smul]
      cases abs_cases ((g • z).re - 1) <;> cases abs_cases (g • z).re <;> linarith

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

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ AnalyticAt ℂ (cuspFunction h (-g)) 0

Tactic:
simpa [cuspFunction_neg hg.continuousAt] using hg.neg

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✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
⊢ 0 < n →
    (∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖) →
      ‖(PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)‖ ≤ 1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖

Tactic:
hn

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
⊢ (∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖) →
    ‖(PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)‖ ≤ 1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
by
  by_cases h : b = 0 ∧ n = 0
  · simp [h.1, h.2]
  · simp only [not_and] at h
    by_cases hb : b = 0
    · 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
    · have h0 : (b : ℂ) * z + n + 1 ≠ 0 := by
        simpa [add_assoc] using linear_ne_zero (cd := ![b, n + 1]) z (by aesop)
      have h1 : (b : ℂ) * z + n ≠ 0 := linear_ne_zero (cd := ![b, n]) z (by aesop)
      simp [δ]
      grind

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

Goal state before:
pp: hη : DifferentiableOn ℂ η upperHalfPlaneSet
⊢ DifferentiableOn ℂ (E2 ∘ ↑ofComplex) {z | 0 < z.im}

Tactic:
have hlog : DifferentiableOn ℂ (logDeriv η) _ :=
    (hη.deriv isOpen_upperHalfPlaneSet).div hη (fun _ hz ↦ eta_ne_zero hz)

Goal state after:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
⊢ DifferentiableOn ℂ (E2 ∘ ↑ofComplex) {z | 0 < z.im}
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hcusp : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ qExpansion 1 (Δ * ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))) =
    qExpansion 1 Δ * qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))

Tactic:
← CuspForm.coe_discriminant

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hcusp : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ qExpansion 1 (⇑CuspForm.discriminant * ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))) =
    qExpansion 1 ⇑CuspForm.discriminant * qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
rw [rank_eq_one_add_rank_cuspForm hk.1 hk2, CuspForm.discriminantEquiv.rank_eq,
      levelOne_neg_weight_rank_zero (by lia)]
    have : k ∈ (Finset.Icc 3 11).filter Even := by grind
    fin_cases this <;> simp [Nat.ModEq]

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

Goal state before:
pp: case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2
⊢ rexp (↑π * I * ↑n ^ 2 * τ).re = y ^ n ^ 2

Tactic:
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (sq_nonneg n)

Goal state after:
case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (↑π * I * ↑n ^ 2 * τ).re = y ^ n ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: this : IsClosed {z | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
x : ℂ
x✝ : x ∈ {z | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
him : 0 ≤ x.im
hre : 1 ≤ ‖x‖
hnorm : |x.re| ≤ 1 / 2
⊢ 0 < x.im

Tactic:
exact him.lt_of_ne' <| by grind [abs_re_eq_norm]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

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

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

Tactic:
· simp only [emultiplicity_zero, add_top, pow_zero, sub_self]

Goal state after:
case succ
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
⊢ emultiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)
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
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ (↑2 * ↑n / ↑(h Γ)) ^ s = ↑2 ^ s * ↑n ^ s / ↑(h Γ) ^ s

Tactic:
← ofReal_natCast,

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
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ (↑2 * ↑↑n / ↑(h Γ)) ^ s = ↑2 ^ s * ↑↑n ^ s / ↑(h Γ) ^ s
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x - y)
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = emultiplicity ↑p ↑(x - y) + emultiplicity p n

Tactic:
Int.natCast_sub hyx

Goal state after:
case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑x - ↑y
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = emultiplicity (↑p) (↑x - ↑y) + emultiplicity p n
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ ↑(padicValNat 2 (x ^ n - y ^ n)) + ↑1 = ↑(padicValNat 2 (x + y)) + ↑(padicValNat 2 (x - y)) + ↑(padicValNat 2 n)

Tactic:
iterate 4 rw [padicValNat_eq_emultiplicity]

Goal state after:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + ↑1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ n ≠ 0

x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x - y ≠ 0

x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x + y ≠ 0

x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x ^ n - y ^ n ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

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

Tactic:
refine measurable_fst.prodMk <| Measurable.comp ?_ measurable_snd
  exact measurable_pi_lambda _
    fun _ ↦ continuous_polarCoord_symm.measurable.comp (measurable_pi_apply _)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) ≠ 0

Tactic:
norm_unit

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ 1 ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * x) = (logEmbedding K) (Additive.ofMul u) + logMap x

Tactic:
logMap_mul (by rw [norm_unit]; norm_num) hx,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) + logMap x = (logEmbedding K) (Additive.ofMul u) + logMap x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ ¬(|c| ^ Module.finrank ℚ K = 0 ∨ mixedEmbedding.norm x = 0)

Tactic:
not_or

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬mixedEmbedding.norm x = 0
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : ∃! y, y ≠ 1
⊢ σ = τ

Tactic:
exact ExistsUnique.unique this
    ((isConj_ne_one_iff hφ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ)
    ((isConj_ne_one_iff hψ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal ψ)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ mixedEmbedding.norm (↑u • ↑b) = mixedEmbedding.norm ↑b

Tactic:
norm_unit_smul

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ mixedEmbedding.norm ↑b = mixedEmbedding.norm ↑b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
⊢ x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A

Tactic:
simp_rw [Set.mem_preimage, Set.mem_image, normAtAllPlaces_norm_at_real_places]

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

Goal state before:
pp: case e'_2.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
e_1✝ : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑J } = ↑{a | ↑(preimageOfMemIntegerSet a) ∈ ↑↑J}
x✝ : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑J }
⊢ mixedEmbedding.norm ↑↑x✝ = ↑n ↔ mixedEmbedding.norm ↑((idealSetEquiv K J).symm x✝) = ↑n

Tactic:
idealSetEquiv_symm_apply

Goal state after:
case e'_2.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
e_1✝ : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑J } = ↑{a | ↑(preimageOfMemIntegerSet a) ∈ ↑↑J}
x✝ : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑J }
⊢ mixedEmbedding.norm ↑↑x✝ = ↑n ↔ mixedEmbedding.norm ↑↑x✝ = ↑n
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ LinearIndependent ℝ fun x ↦ ↑((basisUnitLattice K) (equivFinRank.symm x))

Tactic:
convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ ↑((basisUnitLattice K) (equivFinRank.symm x✝)) =
    ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).reindex equivFinRank) x✝
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
⊢ (Subgroup.closure (Set.range v) ⊔ torsion K).FiniteIndex

Tactic:
← finiteIndex_iff_sup_torsion_finiteIndex

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
⊢ (Subgroup.closure (Set.range v)).FiniteIndex
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P.ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, ramificationIdx_span_zeta_sub_one]

Goal state after:
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
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ (span {hζ.toInteger - 1}).IsPrime

Tactic:
rw [← pow_one p] at hK hζ

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 ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ (span {hζ✝.toInteger - 1}).IsPrime
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
h : 2 < p
⊢ ¬hζ.toInteger - 1 ∣ 2

Tactic:
rw [← pow_one p] at hK hζ

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
h : 2 < p
⊢ ¬hζ✝.toInteger - 1 ∣ 2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) ↑p

Tactic:
← eval_one_cyclotomic_prime (R := 𝓞 K) (p := p),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) (eval 1 (cyclotomic p (𝓞 K)))