mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable

Goal state before:
pp: k : ℤ
a : Fin 2 → ℤ
z : ℂ
hz : z ∈ {z | 0 < z.im}
⊢ (eisSummand k a ∘ ↑ofComplex) z = (↑(a 0) * z + ↑(a 1)) ^ (-k)

Tactic:
lift z to ℍ using hz

Goal state after:
k : ℤ
a : Fin 2 → ℤ
z : ℍ
⊢ (eisSummand k a ∘ ↑ofComplex) ↑z = (↑(a 0) * ↑z + ↑(a 1)) ^ (-k)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ 0 ≤ ↑(-g) 1 1

Tactic:
simpa using (not_le.mp hd).le

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: n : ℕ+
k l : ℕ
h : (k, l) ∈ (↑n).divisorsAntidiagonal
⊢ (fun x ↦ ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩) ((fun x ↦ divisorsAntidiagonalFactors x.fst x.snd) ⟨n, ⟨(k, l), h⟩⟩) =
    ⟨n, ⟨(k, l), h⟩⟩

Tactic:
rw [Nat.mem_divisorsAntidiagonal] at h

Goal state after:
n : ℕ+
k l : ℕ
h✝ : (k, l) ∈ (↑n).divisorsAntidiagonal
h : (k, l).1 * (k, l).2 = ↑n ∧ ↑n ≠ 0
⊢ (fun x ↦ ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩)
      ((fun x ↦ divisorsAntidiagonalFactors x.fst x.snd) ⟨n, ⟨(k, l), h✝⟩⟩) =
    ⟨n, ⟨(k, l), h✝⟩⟩
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ ↑m‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ (↑n * ↑m) = (1 - r ^ ↑m)⁻¹ - 1
⊢ Tendsto (fun x ↦ r ^ ↑x) atTop (𝓝 0)

Tactic:
exact (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).comp <| tendsto_PNat_val_atTop_atTop

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
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)) =O[atTop] fun n ↦ ↑n ^ (↑k / 2)

Tactic:
by
  apply qExpansion_coeff_isBigO_of_norm_isBigO
  obtain ⟨C, hC⟩ := exists_bound f
  refine isBigO_of_le' (c := C) _ fun τ ↦ (hC τ).trans (of_eq ?_)
  rw [Real.norm_of_nonneg (by positivity), Real.rpow_neg τ.im_pos.le, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ Icc (-↑x) ↑x = Icc (-(↑x - 1)) (↑x - 1) ∪ {-↑x, ↑x}

Tactic:
convert! Finset.Icc_succ_succ (x - 1) (x - 1) <;> grind

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
z : ℍ
⊢ (serreDerivative (↑k) F ∣[k + 2] γ) z =
    (D F ∣[k + 2] γ) z - ↑k * 12⁻¹ * ((EisensteinSeries.E2 ∣[2] γ) z * (F ∣[k] γ) z)

Tactic:
grind [ModularForm.SL_slash_apply, serreDerivative_apply, Pi.mul_apply,
      congrFun (ModularForm.mul_slash_SL2 2 k γ EisensteinSeries.E2 F) z]

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

Goal state before:
pp: hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
τ : ℍ
hτ : dist (∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 ↑τ‖ = rexp (-2 * π * τ.im)
hsub : ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24 - 1‖ < 1 / 2
⊢ 1 / 2 ≤ ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24‖

Tactic:
have h1 := norm_sub_norm_le 1 (∏' n, (1 - eta_q n τ) ^ 24)

Goal state after:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
τ : ℍ
hτ : dist (∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 ↑τ‖ = rexp (-2 * π * τ.im)
hsub : ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24 - 1‖ < 1 / 2
h1 : ‖1‖ - ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24‖ ≤ ‖1 - ∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24‖
⊢ 1 / 2 ≤ ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ HasSum (fun m ↦ (if m = 0 then 1 else -24 * ↑((σ 1) m)) • cexp (2 * ↑π * I * ↑z) ^ m) (E2 z)

Tactic:
rw [← hasSum_nat_add_iff' 1]

Goal state after:
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ HasSum (fun n ↦ (if n + 1 = 0 then 1 else -24 * ↑((σ 1) (n + 1))) • cexp (2 * ↑π * I * ↑z) ^ (n + 1))
    (E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
⊢ FiniteDimensional ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)

Tactic:
by
  rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]
  rcases lt_or_ge k 0 with hk_neg | hk_nonneg
  · rw [levelOne_neg_weight_rank_zero hk_neg]
    exact Cardinal.aleph0_pos
  rcases Int.even_or_odd k with hk_even | hk_odd
  · lift k to ℕ using hk_nonneg
    rw [dimension_level_one k (mod_cast hk_even)]
    split_ifs <;> exact_mod_cast Cardinal.natCast_lt_aleph0
  · rw [levelOne_odd_weight_rank_zero hk_odd]
    exact Cardinal.aleph0_pos

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
⊢ g • I = I ↔ g ∈ {1, -1, S, -S}

Tactic:
constructor
  · intro hg
    have := cases_of_mem_fd_smul_mem_fd I_mem_fd (hg.symm ▸ I_mem_fd)
    norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, ρ] at this
    grind
  · suffices S • I = I by simp +contextual [-sl_moeb, or_imp, this]
    rw [modular_S_smul, UpperHalfPlane.ext_iff]
    norm_num

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

Goal state before:
pp: case e'_5
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ) * 2) (jacobiTheta τ - 1)
⊢ (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) = fun i ↦ cexp (↑π * I * (↑i + 1) ^ 2 * τ) * 2 / 2

Tactic:
mul_div_cancel_right₀ _ (two_ne_zero' ℂ)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ 1 < 1 + ↑a ^ 2 + 2 * ↑a * x.im

Tactic:
add_assoc,

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ 1 < 1 + (↑a ^ 2 + 2 * ↑a * x.im)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ HasSum (fun m ↦ c m • 𝕢 1 ↑τ ^ m) ((E hk) τ)

Tactic:
rw [← hasSum_nat_add_iff' 1]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ HasSum (fun n ↦ c (n + 1) • 𝕢 1 ↑τ ^ (n + 1)) ((E hk) τ - ∑ i ∈ Finset.range 1, c i • 𝕢 1 ↑τ ^ i)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.re ^ 2 ≤ (1 / 2) ^ 2

Tactic:
rw [sq_le_sq, abs_of_pos <| one_half_pos (α := ℝ)]
      exact hz.2.2.1

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

Tactic:
have h1 : τ.im ≤ (γ • τ).im := h.trans hγ

Goal state after:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ (γ • τ).im
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: ⊢ Tendsto (UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)) atTop atTop

Tactic:
refine tendsto_id.congr' ?_

Goal state after:
⊢ id =ᶠ[atTop] UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ⇑f = 0
τ : ℍ
⊢ 1 ∈ ℋ ∧ (⇑f ∣[k] 1⁻¹) τ = 0

Tactic:
by simpa using congr_fun hf τ

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K∞
hx : ¬IsUnit x
⊢ ‖x‖ = 0

Tactic:
rw [Pi.isUnit_iff, not_forall] at hx
  obtain ⟨v, hv⟩ := hx
  exact Finset.prod_eq_zero_iff.2 ⟨v, Finset.mem_univ v, by simpa [isUnit_iff_ne_zero] using hv⟩

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(∑ x ∈ range p, x))) = 0

Tactic:
simp only [Finset.sum_range_id]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0
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
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
⊢ HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)

Tactic:
rw [hΛ]
  have hh := Γ.strictWidthInfty_pos
  have hΓ := Γ.strictWidthInfty_mem_strictPeriods
  refine hasSum_mellin_pi_mul₀ (fun _ ↦ by positivity) hpos ?_ ?_
  · -- show `q`-expansion converges to `f` on positive imaginary axis
    intro t (ht : 0 < t)
    have := hasSum_qExpansion f hh hΓ (ofComplex (I * t))
    convert! hasSum_ite_sub_hasSum this 0 using 2 with n
    · rcases Nat.eq_zero_or_pos n with rfl | hn
      · simp
      · simp [hn.ne', Function.Periodic.qParam, ofComplex_apply_eq_ite, ht, ← exp_nat_mul]
        grind [I_sq]
    · simp only [weakFEPair]
      rw [qExpansion_coeff_zero hh, pow_zero, mul_one]
      · exact ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ
      · exact SlashInvariantFormClass.periodic_comp_ofComplex f hΓ
  · -- show summability of Dirichlet series
    simp_rw [mul_comm (2 : ℝ), mul_div_assoc,
      Real.mul_rpow (Nat.cast_nonneg _) (show 0 ≤ 2 / h Γ by positivity), ← div_div]
    apply Summable.div_const
    apply summable_of_isBigO_nat (Real.summable_nat_rpow.mpr <| show r - s.re < -1 by linarith)
    simp only [Real.rpow_sub' (Nat.cast_nonneg _) (show r - s.re ≠ 0 by linarith)]
    apply IsBigO.mul _ (isBigO_refl _ _)
    simpa using hcoeff.norm_left

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: w✝ : ℤ
⊢ (1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1

Tactic:
add_assoc,

Goal state after:
w✝ : ℤ
⊢ (1 + (w✝ * 4 + w✝ ^ 2 * 4)) % 4 = 1
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝¹ i] (A i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
have := weaklyLocallyCompactSpace_of_principal hS hSA

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝¹ i] (A i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
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 : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ ∫⁻ (a : mixedSpace K), A.indicator 1 a ∂volume =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
← lintegral_comp_polarSpaceCoord_symm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ ∫⁻ (x : polarSpace K) in (polarSpaceCoord K).target,
      (∏ w, ENNReal.ofReal (x.1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm x) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)
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 : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        ⇑mixedSpaceOfRealSpace ⁻¹' normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A ∩
          Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
        (fun x ↦ ∏ x, ENNReal.ofReal (a ↑x)) a ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume

Tactic:
rw [hA, volume_eq_two_pi_pow_mul_integral_aux hA]

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
        (fun x ↦ ∏ x, ENNReal.ofReal (a ↑x)) a ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in
        ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0,
        ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ ⊥.inertiaDeg v.Completion = Module.finrank v.Completion w.Completion

Tactic:
Ideal.inertiaDeg_eq_of_isMaximal ⊥

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ Module.finrank (v.Completion ⧸ ⊥) (w.Completion ⧸ ⊥) = Module.finrank v.Completion w.Completion
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x✝ : v.Completion
⊢ ((((algebraMap v.Completion w.Completion).comp (RingEquiv.quotientBot v.Completion).toRingHom).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion =
    ((((RingEquiv.quotientBot w.Completion).toRingHom.comp (algebraMap (v.Completion ⧸ ⊥) (w.Completion ⧸ ⊥))).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
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
⊢ ∀ (b : InfinitePlace K),
    ¬b = w' →
      (if h : b = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b, ⋯⟩))))) = 0

Tactic:
intro _ h

Goal state after:
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
b✝ : InfinitePlace K
h : ¬b✝ = w'
⊢ (if h : b✝ = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b✝, ⋯⟩))))) = 0
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p 1
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p 1
⊢ ζ - 1 ∣ η₁ - η₂

Tactic:
rcases eq_or_ne η₁ η₂ with rfl | h
  · simp
  · exact (hζ.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime hp hη₁ hη₂ h).dvd

Goal state after:
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
⊢ regOfFamily u / regOfFamily v =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
classical
  by_cases hu : IsMaxRank u
  · have : span ℤ (Set.range (basisOfIsMaxRank hu)) ≤ span ℤ (Set.range (basisOfIsMaxRank hv)) := by
      rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]
      exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h
    rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv,
      covolume_div_covolume_eq_relIndex _ _ this, span_basisOfIsMaxRank hu,
      span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker,
      ← OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]
  · rw [regOfFamily_eq_zero hu, zero_div, eq_comm, Nat.cast_eq_zero]
    have : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0 := by
      rw [← Subgroup.finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex]
      exact isMaxRank_iff_closure_finiteIndex.mp hv
    rwa [← mul_eq_zero_iff_right this, Subgroup.relIndex_mul_index h,
      ← Subgroup.not_finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex,
      ← isMaxRank_iff_closure_finiteIndex.not]

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

Goal state before:
pp: case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + 1 + 1)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + 1 + 1))
⊢ Associated ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p

Tactic:
add_assoc,

Goal state after:
case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + (1 + 1))} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + (1 + 1)))
⊢ Associated ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p
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
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ ¬span {hζ.toInteger - 1} ∣ span {x}

Tactic:
dvd_span_singleton,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ x ∉ span {hζ.toInteger - 1}
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l : β
⊢ ∑ x_1, ↑(x (l, x_1)) * ∑ u, ↑(a' K a k l x_1 u) * (newBasis K) u = (fun j ↦ a k j) l * ξ K x l

Tactic:
ξ,

Goal state after:
case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l : β
⊢ ∑ x_1, ↑(x (l, x_1)) * ∑ u, ↑(a' K a k l x_1 u) * (newBasis K) u =
    (fun j ↦ a k j) l * ∑ r, ↑(x (l, r)) * (newBasis K) r
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))

Tactic:
have := (tendsto_norm_le_div_atTop₀ K).add tendsto_inv_atTop_zero
  rw [add_zero] at this
  apply this.congr'
  filter_upwards [eventually_ge_atTop 0] with s hs
  simp_rw [← Nat.le_floor_iff hs]
  rw [Ideal.card_norm_le_eq_card_norm_le_add_one, Nat.cast_add, Nat.cast_one, add_div, one_div]

Goal state after:
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ CompactSpace ℤ_[p]

Tactic:
by
  rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete]
  exact ⟨totallyBounded_univ p, isComplete_univ⟩

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ 1 * f ↑p ^ k + 1 * f ↑m ^ k < 1

Tactic:
by
    have hm₀ : 0 < f m := f.pos <| Nat.cast_ne_zero.mpr fun H ↦ hpm <| H ▸ dvd_zero p
    linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]

Goal state after: