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

Goal state before:
pp: case neg.refine_1.ind.succ
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x ↦ ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x ↦ 0
n : ℕ
ih : ∀ m < n + 1, F m = 0
⊢ Tendsto (fun x ↦ ↑(n + 1) ^ ↑x * LSeries F ↑x) atTop (nhds (F (n + 1)))

Tactic:
simpa using! LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
            Ne.lt_top ha

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

Goal state before:
pp: case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), ¬n = 0 → f n = 0
x : ℝ
⊢ (fun x ↦ LSeries f ↑x) x = 0 x

Tactic:
simp [LSeries_congr (fun {n} ↦ H n) x, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl]

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

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
t : ℝ
ht : 0 < t
⊢ t ^ (-s) = t * (t ^ (-s) / t ^ 1)

Tactic:
Real.rpow_one,

Goal state after:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
t : ℝ
ht : 0 < t
⊢ t ^ (-s) = t * (t ^ (-s) / t)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare ↑a

Tactic:
exact legendreSym.eq_neg_one_iff p

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

Goal state before:
pp: a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬¬IsSquare ↑a

Tactic:
rw [← nonsquare_iff_jacobiSym_eq_neg_one, h]; decide

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

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ (↑2).gcd ↑b = 1

Tactic:
Int.gcd_natCast_natCast,

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ Nat.gcd 2 b = 1
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : K
⊢ x ∈ 𝒪[K] ↔ ‖x‖ ≤ 1

Tactic:
simp [Valuation.mem_integer_iff, ← NNReal.coe_le_coe]

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

Goal state before:
pp: case ind.isFalse.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : b % a = 0
⊢ (↑a).gcd ↑b ≠ 1

Tactic:
Int.gcd_natCast_natCast,

Goal state after:
case ind.isFalse.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : b % a = 0
⊢ a.gcd b ≠ 1
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
⊢ {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), |↑(p.coeff ↑i)| ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

Tactic:
abs_le

Goal state after:
n : ℕ
B : ℝ≥0
⊢ {p |
        p.natDegree ≤ n ∧
          ∀ (i : Fin (n + 1)), -(↑(n.choose ↑i) * ↑B) ≤ ↑(p.coeff ↑i) ∧ ↑(p.coeff ↑i) ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ω_mul_ωb

Goal state after:
q : ℕ
⊢ 1 = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ (1 + α) ^ 2 = 2 * ω

Tactic:
ext <;> simp [α, ω, sq]

Goal state after:
case h₁
q : ℕ
⊢ 1 + 3 = 2 * 2

case h₂
q : ℕ
⊢ 1 + 1 = 2
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mp
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ⟨x, hx✝⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
simp only [Subgroup.mem_top, true_and] at hxx

Goal state after:
case mp
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 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)
⊢ (fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯)
      ((fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p) p) =
    p

Tactic:
induction p using ind with | h w hw =>
    by_cases h₀ : w 1 = 0 <;> simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
        if_false, OnePoint.elim_infty, OnePoint.elim_some]
    · have : w 0 ≠ 0 := fun h ↦ hw <| funext <| by simp_all
      use (w 0)⁻¹
      ext i
      fin_cases i <;> simp_all
    · exact ⟨(w 1)⁻¹, funext <| by simp [inv_mul_cancel₀ h₀]⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ |(g • z).re| ≤ 1 / 2

Tactic:
abs_le

Goal state after:
case right
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ -(1 / 2) ≤ (g • z).re ∧ (g • z).re ≤ 1 / 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable

Goal state before:
pp: case inr
k : ℤ
⊢ DifferentiableOn ℂ (fun z ↦ (↑(0 0) * z + ↑(0 1)) ^ (-k)) {z | 0 < z.im}

Tactic:
simp only [Pi.zero_apply, Int.cast_zero, zero_mul, add_zero]

Goal state after:
case inr
k : ℤ
⊢ DifferentiableOn ℂ (fun z ↦ 0 ^ (-k)) {z | 0 < z.im}
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
⊢ HasFPowerSeriesOnBall (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1

Tactic:
have h2 : HasFPowerSeriesAt (cuspFunction h f) (qExpansionFormalMultilinearSeries h f) 0 := by
    simpa [qExpansionFormalMultilinearSeries, qExpansion_coeff, div_eq_mul_inv, mul_comm]
      using hfanalytic.hasFPowerSeriesAt

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
h2 : HasFPowerSeriesAt (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0
⊢ HasFPowerSeriesOnBall (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) -
      (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • (PowerSeries.coeff 0) (qExpansion 1 ⇑g) =
    0

Tactic:
simp [hg]

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

Goal state before:
pp: case hg
z : ℍ
⊢ Summable (fun n ↦ ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) (symmetricIco ℤ)

pp: z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
· apply HasSum.summable (a := -2 * π * I / z)
    rw [hasSum_symmetricIco_int_iff, ← tendsto_comp_val_Ioi_atTop]
    exact tendsto_tsum_one_div_linear_sub_succ_eq z

Goal state after:
z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
⊢ D (F ∣[k] g) = fun z ↦
    (↑(↑g).det)⁻¹ * (D F ∣[k + 2] g) z - ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F ∣[k] g) z

Tactic:
have hdetℂ : (g.val.det : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr hg.ne'

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
⊢ D (F ∣[k] g) = fun z ↦
    (↑(↑g).det)⁻¹ * (D F ∣[k + 2] g) z - ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F ∣[k] g) z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
hE2 : (E2 ∣[2] ModularGroup.S) z = (E2 - (1 / (2 * riemannZeta 2)) • D2 ModularGroup.S) z
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = deriv sqrt ↑z / (↑z).sqrt + logDeriv η ↑z

Tactic:
simp only [one_div, SL_slash_def, modular_S_smul, ModularGroup.denom_S,
    Int.reduceNeg, zpow_neg, riemannZeta_two, mul_inv_rev, inv_div, Pi.sub_apply, Pi.smul_apply,
    D2, ModularGroup.denom_S, smul_eq_mul] at hE2

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = deriv sqrt ↑z / (↑z).sqrt + logDeriv η ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
this : η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
⊢ (Δ ∣[12] ModularGroup.S) z = Δ z

Tactic:
by
    rw [SL_slash_apply, UpperHalfPlane.modular_S_smul]
    simpa [denom, ModularGroup.S]

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

Goal state before:
pp: ⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine .congr (fun z hz ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).pow
      24 |>.differentiableWithinAt) fun z hz ↦ ?_

Goal state after:
z : ℂ
hz : z ∈ {z | 0 < z.im}
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
⊢ DifferentiableOn ℂ (iteratedDerivWithin a (fun z ↦ cexp (2 * ↑π * I * z) ^ n) s) s

Tactic:
suffices DifferentiableOn ℂ (iteratedDeriv a (fun z ↦ cexp (2 * π * I * z) ^ n)) s by
    apply this.congr (iteratedDerivWithin_of_isOpen hs)

Goal state after:
n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
⊢ DifferentiableOn ℂ (iteratedDeriv a fun z ↦ cexp (2 * ↑π * I * z) ^ n) s
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 ⇑E₄ = qExpansion 1 ⇑f ^ 2
⊢ qExpansion 1 (c6 • ⇑E₆) = qExpansion 1 ⇑((f.mul f).mul f)

Tactic:
show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6

Goal state after:
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 ⇑E₄ = qExpansion 1 ⇑f ^ 2
⊢ qExpansion 1 ⇑((f.mul f).mul f) = qExpansion 1 ⇑((f.mul f).mul f)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
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
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
have : k < 3 ∨ (3 ≤ k ∧ k < 12) ∨ 12 ≤ k := by grind

Goal state after:
case h
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
this : k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z
⊢ 1 < (↑k).re

Tactic:
norm_cast; grind

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

Goal state before:
pp: case e'_2.e'_5
z : ℍ
x✝ : ℤ
⊢ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑x✝ * ↑z + ↑n) - 1 / (↑x✝ * ↑z + ↑n + 1)) = 0

Tactic:
exact tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z _

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

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! = -(2 * ↑k / ↑(bernoulli k))

Tactic:
rw [h2, Nat.cast_mul 2 (m + 1), Nat.cast_two, riemannZeta_two_mul_nat (show m + 1 ≠ 0 by grind),
    show (2 * (m + 1))! = 2 * (m + 1) * (2 * m + 1)! by grind [Nat.factorial_succ],
    show 2 * (m + 1) - 1 = 2 * m + 1 by grind, mul_pow, mul_pow, pow_mul I, I_sq]

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        ((-2) ^ (2 * (m + 1)) * ↑π ^ (2 * (m + 1)) * (-1) ^ (m + 1)) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
⊢ (↑p * b) ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)

Tactic:
simp only [sq_dvd_add_pow_sub_sub (↑p * b) a i, ← sub_sub]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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

Tactic:
rw [pow_one, ← even_iff_two_dvd]

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
⊢ Even (x ^ 2 ^ i + y ^ 2 ^ i)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 2 = 1

Tactic:
FiniteMultiplicity.emultiplicity_self

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ 1 = 1

x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ FiniteMultiplicity 2 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ u • x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, smul_zero]⟩
  contrapose! h
  obtain ⟨w, h⟩ := exists_normAtPlace_ne_zero_iff.mpr h
  refine exists_normAtPlace_ne_zero_iff.mp ⟨w, ?_⟩
  rw [unitSMul_smul, map_mul]
  exact mul_ne_zero (by simp) h

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
⊢ normAtComplexPlaces '' A = ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0

Tactic:
have h : ∀ (x : mixedSpace K), ∀ w, IsComplex w → 0 ≤ normAtComplexPlaces x w := by
    intro x w hw
    rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]
    exact norm_nonneg _

Goal state after:
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
⊢ normAtComplexPlaces '' A = ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 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
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
⊢ Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K = realUnits K ⊔ torsion K

Tactic:
rw [realUnits, MonoidHom.range_eq_map, ← closure_fundSystem_sup_torsion_eq_top, Subgroup.map_sup,
    sup_assoc, RingHom.toMonoidHom_eq_coe, sup_eq_right.mpr this, MonoidHom.map_closure]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
⊢ Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K =
    Subgroup.closure (⇑(Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) '' Set.range (fundSystem ↥K⁺)) ⊔ torsion K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs]

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } * torsionOrder K =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }
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 σ)
this : IsTotallyReal ↥L
⊢ Module.finrank (↥L) K = 2

Tactic:
IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup,

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 σ)
this : IsTotallyReal ↥L
⊢ Nat.card ↥(Subgroup.zpowers σ) = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMapBasis x = Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
expMapBasis_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMap ((completeBasis K).equivFun.symm x) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ (reindex g g) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e i))))) i j =
    (of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
      (fun x ↦ f ((f.symm w').succAbove x)) (fun x ↦ f ((f.symm w').succAbove x)) i j

Tactic:
rw [reindex_apply, submatrix_apply, submatrix_apply, of_apply, of_apply, dif_neg]

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ↑(↑(g.symm j)).mult * Real.log (↑(g.symm j) ((algebraMap (𝓞 K) K) ↑(u (e (g.symm i))))) =
    ↑(f ((f.symm w').succAbove j)).mult *
      Real.log ((f ((f.symm w').succAbove j)) ((algebraMap (𝓞 K) K) ↑(u (e ⟨f ((f.symm w').succAbove i), ?e_a.hnc✝⟩))))

case e_a.hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ¬f ((f.symm w').succAbove i) = w'
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap (mixedSpaceOfRealSpace (↑expMapBasis fun i ↦ if i = w₀ then 0 else x i))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
expMapBasis_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap
            (mixedSpaceOfRealSpace (↑expMap ((completeBasis K).equivFun.symm fun i ↦ if i = w₀ then 0 else x i)))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ w, Real.exp ((↑(↑w).mult)⁻¹ * (completeBasis K).equivFun.symm x ↑w)) *
      ∏ w, Real.exp ((↑(↑w).mult)⁻¹ * (completeBasis K).equivFun.symm x ↑w) =
    ((∏ w, ↑expMapBasis x ↑w ^ (↑w).mult) * ∏ w, ↑expMapBasis x ↑w ^ (↑w).mult) * (∏ w, ↑expMapBasis x ↑w)⁻¹

Tactic:
expMapBasis_apply,

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ w, Real.exp ((↑(↑w).mult)⁻¹ * (completeBasis K).equivFun.symm x ↑w)) *
      ∏ w, Real.exp ((↑(↑w).mult)⁻¹ * (completeBasis K).equivFun.symm x ↑w) =
    ((∏ w, ↑expMap ((completeBasis K).equivFun.symm x) ↑w ^ (↑w).mult) *
        ∏ w, ↑expMap ((completeBasis K).equivFun.symm x) ↑w ^ (↑w).mult) *
      (∏ w, ↑expMap ((completeBasis K).equivFun.symm x) ↑w)⁻¹
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
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : (span {hζ.toInteger - 1}).IsPrime
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
have hp0 : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : (span {hζ.toInteger - 1}).IsPrime
hp0 : 𝒑 ≠ ⊥
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)