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

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

Tactic:
have hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0 := by
    simpa [cuspFunction_neg hg.continuousAt] using hg.neg
  simpa [sub_eq_add_neg, qExpansion_neg hg] using (qExpansion_add hf hg')

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

Goal state before:
pp: case mpr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : f = 0
⊢ qExpansion h f = 0

Tactic:
simpa [H] using qExpansion_zero h

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr
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:
· right
    left
    rw [hgz, zpow_neg_one, eq_self_iff_true, true_or, true_and]
    rw [hb, Int.cast_neg, Int.cast_one] at hre
    linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]

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
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖∑ b ∈ Icc (-(x - 1)) (x - 1) ∪ {-x, x}, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖ = ‖f x‖

Tactic:
Finset.sum_union,

Goal state after:
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
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖∑ x ∈ Icc (-(x - 1)) (x - 1), f x + ∑ x ∈ {-x, x}, f x - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖ = ‖f x‖

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
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z + (2 * z.re + 1) ≤ 1
this : normSq (↑z + 1) = normSq ↑z + (2 * z.re + 1)
⊢ normSq ↑z = 1 ∧ z.re = -1 / 2

Tactic:
constructor <;> linarith [hz.1, show 0 ≤ 2 * z.re + 1 by linarith [(neg_le_abs _).trans hz.2]]

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

Goal state before:
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:
obtain ⟨q₀, hq₀, _, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN
      (show ContinuousOn (fun q : ℂ ↦ ‖q‖) K by fun_prop)

Goal state after:
case h.inr
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left✝ : sSup ((fun q ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
⊢ HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℂ
hz : z ∈ ℍₒ
hq : 𝕢 1 z ∈ Metric.ball 0 1
⊢ DifferentiableAt ℂ (fun x ↦ ∏' (n : ℕ), (1 - eta_q n x)) z

Tactic:
exact (differentiableOn_tprod_one_sub_pow.differentiableAt
    (Metric.isOpen_ball.mem_nhds hq)).comp z (by fun_prop)

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

Goal state before:
pp: F : ℍ → ℂ
hF : MDiff F
⊢ MDiff (D F)

Tactic:
by
  rw [UpperHalfPlane.mdifferentiable_iff] at hF ⊢
  let c : ℂ := (2 * π * I)⁻¹
  have hDeriv : DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ofComplex) z) upperHalfPlaneSet := by
    simpa [c] using (hF.deriv isOpen_upperHalfPlaneSet).const_mul ((2 * π * I)⁻¹)
  refine hDeriv.congr ?_
  intro z hz
  simp [normalizedDerivOfComplex, c, Function.comp_apply, ofComplex_apply_of_im_pos hz]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
⊢ (g • z).im = z.im

Tactic:
wlog hden : z.im ≤ (g • z).im

Goal state after:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g • z).im = z.im

g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
· apply (summable_pow_mul_cexp k 1 z).congr
    simp

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ Summable fun b ↦ ∑' (c : ℤ), eisSummand ↑k ![(b, c).1, (b, c).2] z

Tactic:
simpa using (summable_prod_eisSummand hk z).prod

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

Goal state before:
pp: case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
rw [levelOne_odd_weight_rank_zero hk_odd]

Goal state after:
case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ 0 < Cardinal.aleph0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
this : S • ρ ≠ ρ
⊢ g ≠ S ∧ g ≠ -S

Tactic:
grind [SL_neg_smul]

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

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

Tactic:
by
  rcases lt_or_ge k 0 with hk | hk
  · exact rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero hk) f
  · lift k to ℕ using hk
    exact sturm_bound_levelOne_nat (mod_cast h)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this✝ : T • ρ ≠ ρ
this : T⁻¹ • ρ ≠ ρ
⊢ g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹

Tactic:
grind [SL_neg_smul]

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

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

Tactic:
UpperHalfPlane.modular_S_smul,

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta (-↑τ)⁻¹ = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
this : (T * S * T) • ρ ≠ ρ
⊢ g ≠ T * S * T ∧ g ≠ -(T * S * T)

Tactic:
grind [SL_neg_smul]

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

Goal state before:
pp: z : ℍ
⊢ discriminant z = (E₄ z ^ 3 - E₆ z ^ 2) / 1728

Tactic:
obtain ⟨g, hg⟩ := E₄CubeSubE₆SqForm_isCuspForm

Goal state after:
z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
⊢ discriminant z = (E₄ z ^ 3 - E₆ z ^ 2) / 1728
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
r C : ℝ
hCpos : C > 0
hCO : (fun τ ↦ f τ - valueAtInfty ⇑f) =O[atImInfty] fun τ ↦ rexp (-C * τ.im)
⊢ ((fun τ ↦ rexp (-C * τ.im)) ∘ fun t ↦ ↑ofComplex (I * ↑t)) =O[atTop] fun t ↦ t ^ r

Tactic:
refine (EventuallyEq.isBigO ?_).trans (isLittleO_exp_neg_mul_rpow_atTop hCpos r).isBigO

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
r C : ℝ
hCpos : C > 0
hCO : (fun τ ↦ f τ - valueAtInfty ⇑f) =O[atImInfty] fun τ ↦ rexp (-C * τ.im)
⊢ ((fun τ ↦ rexp (-C * τ.im)) ∘ fun t ↦ ↑ofComplex (I * ↑t)) =ᶠ[atTop] fun x ↦ rexp (-C * x)
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 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
x : Πʳ (i : ι₁), [R₁ i, A₁ i]_[𝓕₁]
⊢ ∀ᶠ (i : ι₂) in 𝓕₂, (fun j ↦ φ j (x (f j))) i ∈ (fun j ↦ A₂ j) i

Tactic:
filter_upwards [hf.eventually x.2, hφ] using fun _ h1 h2 ↦ h2 h1

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 1 < v.intValuation d * (valuation K v) k

Tactic:
exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
      mul_le_mul_of_nonneg_right this (by simp)

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

Goal state before:
pp: case e'_3
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : f ∈ DFunLike.coe ⁻¹' (Sᶜ ∩ {i | p i}).pi A
i : ι
hiT : p i
⊢ ↑f i ∈ A i

Tactic:
by_cases hiS : i ∈ S

Goal state after:
case pos
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : f ∈ DFunLike.coe ⁻¹' (Sᶜ ∩ {i | p i}).pi A
i : ι
hiT : p i
hiS : i ∈ S
⊢ ↑f i ∈ A i

case neg
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : f ∈ DFunLike.coe ⁻¹' (Sᶜ ∩ {i | p i}).pi A
i : ι
hiT : p i
hiS : i ∉ S
⊢ ↑f i ∈ A 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
this : emultiplicity 2 ↑2 = 1
⊢ emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑d + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (emultiplicity 2 ↑2 + emultiplicity 2 ↑d)

Tactic:
by rw [this, add_comm 1, ← add_assoc]

Goal state after:
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:
simp only [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]

Goal state after:
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)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w, (x.2 w).1

Tactic:
have : (FDerivPolarCoordRealSymm K x).toLinearMap =
      LinearMap.prodMap (LinearMap.id) (fderivPiPolarCoordSymm x.2).toLinearMap := rfl
  rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul,
    ← ContinuousLinearMap.det, det_fderivPiPolarCoordSymm]

Goal state after:
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
⊢ ¬mixedEmbedding.norm (c • x) = 0

Tactic:
mixedEmbedding.norm_smul,

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 * mixedEmbedding.norm x = 0
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)
⊢ volume A =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
rw [← lintegral_indicator_one hm, ← lintegral_comp_polarSpaceCoord_symm, polarSpaceCoord_target',
    Measure.volume_eq_prod, setLIntegral_prod]

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 : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      ∫⁻ (y : { w // w.IsComplex } → ℝ) in Set.univ.pi fun x ↦ Set.Ioo (-π) π,
        (∏ w, ENNReal.ofReal ((x, y).1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm (x, y)) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

case hf
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)
⊢ AEMeasurable (fun x ↦ (∏ w, ENNReal.ofReal (x.1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm x))
    ((volume.prod volume).restrict
      ((Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π))
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑((ringOfIntegersComplexConj K) x) = ↑x
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))

Tactic:
coe_ringOfIntegersComplexConj,

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : (complexConj K) ↑x = ↑x
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
⊢ (normAtPlace w) (mixedSpaceOfRealSpace (normAtAllPlaces x)) = (normAtPlace w) x

Tactic:
normAtPlace_mixedSpaceOfRealSpace (normAtPlace_nonneg w x)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
⊢ normAtAllPlaces x w = (normAtPlace w) x
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
⊢ (algebraMap F K).fieldRange = maximalRealSubfield K

Tactic:
have := IsTotallyReal.ofRingEquiv (algebraMap F K).rangeRestrictFieldEquiv
    have : IsQuadraticExtension (algebraMap F K).fieldRange K :=
    { finrank_eq_two' :=
        (IsQuadraticExtension.finrank_eq_two F K) ▸ Algebra.finrank_eq_of_equiv_equiv
          (algebraMap F K).rangeRestrictFieldEquiv.symm (RingEquiv.refl K) (by ext; simp; rfl) }
    exact eq_maximalRealSubfield K (algebraMap F K).fieldRange

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
h : span {↑p} ≠ ⊥
⊢ (span {↑p}).primesOver (𝓞 K) = {J | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))}

Tactic:
by ext; simp [mem_primesOver_iff_mem_normalizedFactors _ h]

Goal state after:
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 fun w ↦
          (0 • (completeBasis K) w₀ + ∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i) ↑w)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
zero_smul,

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 fun w ↦
          (0 + ∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i) ↑w)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx✝ : x ∈ torsion K
hx : x ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
y : (𝓞 K)ˣ
hy✝ : y ∈ torsion K
hy : y ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
h : I.torsionMapQuot ⟨x, hx✝⟩ = I.torsionMapQuot ⟨y, hy✝⟩
⊢ ⟨x, hx✝⟩ = ⟨y, hy✝⟩

Tactic:
rw [Subtype.mk_eq_mk, ← Subtype.mk_eq_mk (h := hx) (h' := hy)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx✝ : x ∈ torsion K
hx : x ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
y : (𝓞 K)ˣ
hy✝ : y ∈ torsion K
hy : y ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
h : I.torsionMapQuot ⟨x, hx✝⟩ = I.torsionMapQuot ⟨y, hy✝⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : realSpace K) in s, ENNReal.ofReal |(fderiv_expMapBasis K x).det| * f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
          f (↑expMapBasis x)

Tactic:
abs_det_fderiv_expMapBasis

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : realSpace K) in s,
      ENNReal.ofReal
          (Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
            regulator K) *
        f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
          f (↑expMapBasis x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case h_fin
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (interior (normLeOne K)) ≠ ∞

Tactic:
refine lt_top_iff_ne_top.mp <| lt_of_le_of_lt (measure_mono interior_subset) ?_

Goal state after:
case h_fin
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (normLeOne K) < ∞
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case h1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
τ : K →ₐ[ℚ] ℂ
a✝ : τ ∈ univ.erase σ'
⊢ ‖τ α‖ ≤ house α

Tactic:
apply norm_embedding_le_house

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
x✝ : Fin l.zipIdx.length
⊢ y ^ l.zipIdx[↑x✝].2 = y ^ ↑(e x✝)

Tactic:
by simp [e]

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

Goal state before:
pp: case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
x✝¹ : euclidean.mixedSpace K
x✝ : ℝ
h : 0 ≤ x✝
⊢ mixedEmbedding.norm (x✝ • (toMixed K) x✝¹) =
    x✝ ^ Module.finrank ℝ (euclidean.mixedSpace K) * mixedEmbedding.norm ((toMixed K) x✝¹)

Tactic:
mixedEmbedding.norm_smul,

Goal state after:
case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
x✝¹ : euclidean.mixedSpace K
x✝ : ℝ
h : 0 ≤ x✝
⊢ |x✝| ^ Module.finrank ℚ K * mixedEmbedding.norm ((toMixed K) x✝¹) =
    x✝ ^ Module.finrank ℝ (euclidean.mixedSpace K) * mixedEmbedding.norm ((toMixed K) x✝¹)
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, ball y ε

Tactic:
refine ⟨Nat.cast '' Finset.range (p ^ k), Set.toFinite _, fun z _ ↦ ?_⟩

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z ∈ ⋃ y ∈ Nat.cast '' ↑(Finset.range (p ^ k)), ball y ε
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
⊢ 1 < m

Tactic:
contrapose! hm

Goal state after:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hfm1 : 1 < f ↑m
hm : m ≤ 1
⊢ f ↑m ≤ 1
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Δ_[1]^[n] (⇑(mahlerSeries a)) 0 = Δ_[1]^[n] (fun k ↦ ∑ j ∈ range (n + 1), k.choose j • a j) 0

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, zero_add]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • (mahlerSeries a) (x • 1) =
    ∑ x ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • ∑ x_1 ∈ range (n + 1), (x • 1).choose x_1 • a x_1