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

Goal state before:
pp: case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * g (f c) ((fun i ↦ i) ⟨1, ⋯⟩) = c ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
change (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1

Goal state after:
case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * (starRingEnd ℂ) (f c)).im = c 1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖(PowerSeries.coeff n) (qExpansion h ⇑f)‖ * ‖↑↑r ^ n‖

Tactic:
← norm_mul

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖(PowerSeries.coeff n) (qExpansion h ⇑f) * ↑↑r ^ n‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑(↑g 1 0) * ↑z + ↑(↑g 1 1) ≠ 0
⊢ ↑z * ↑(↑g 1 0) + ↑(↑g 1 1) ≠ 0

Tactic:
convert! nonZ2 using 1

Goal state after:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑(↑g 1 0) * ↑z + ↑(↑g 1 1) ≠ 0
⊢ ↑z * ↑(↑g 1 0) + ↑(↑g 1 1) = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: v : Fin 2 → ℤ
⊢ v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)

Tactic:
by
  rw [gammaSet_one_mem_iff, Int.isCoprime_iff_gcd_eq_one]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
by
  have had := g.det_coe
  replace had : g 0 0 * g 1 1 = 1 := by rw [det_fin_two, hc] at had; lia
  rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)
  · use g 0 1
    suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]
    ext i j; fin_cases i <;> fin_cases j <;>
      simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
  · use -(g 0 1)
    suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
    ext i j; fin_cases i <;> fin_cases j <;>
      simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
⊢ ‖(eisensteinSeriesSIF (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) A)) k)
        (ModularGroup.T ^ (↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
apply le_trans (norm_le_tsum_norm N (a ᵥ* A) k hk _)

Goal state after:
N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
⊢ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ (↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
⊢ TendstoLocallyUniformly (fun s x ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x ↦ eisensteinSeries a k x) Filter.atTop

Tactic:
have p_sum : Summable fun x : gammaSet N 1 a ↦ ‖x.val‖ ^ (-k) :=
    mod_cast (summable_one_div_norm_rpow hk').subtype (· ∈ gammaSet N 1 a)

Goal state after:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
⊢ TendstoLocallyUniformly (fun s x ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x ↦ eisensteinSeries a k x) Filter.atTop
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case refine_1
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 : ℝ := ⋯
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
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := ⋯
hne : ‖↑n ^ e‖ = ↑n ^ e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * ↑n ^ e)
⊢ Continuous F

Tactic:
fun_prop (disch := simp [Function.Periodic.qParam_ne_zero])

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

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

Tactic:
have : -F = (-1 : ℂ) • F := by ext; simp
  rw [this, normalizedDerivOfComplex_smul _ _ hF]
  ext
  simp

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

Goal state before:
pp: z : ℍ
⊢ Δ z = 𝕢 1 ↑z * ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24

Tactic:
simp only [discriminant, eta, mul_pow]

Goal state after:
z : ℍ
⊢ 𝕢 24 ↑z ^ 24 * (∏' (n : ℕ), (1 - eta_q n ↑z)) ^ 24 = 𝕢 1 ↑z * ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ HasSum (fun x ↦ e2Summand x z)
    (2 * riemannZeta 2 - 8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n) (symmetricIcc ℤ)

Tactic:
simpa [HasSum, -symmetricIcc_filter, symmetricIcc_eq_map_Icc_nat, Function.comp_def,
    G2_partial_sum_eq] using! (aux_G2_tendsto z).const_add _

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

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

Tactic:
· -- `12 ≤ k`: rank decomposition + induction hypothesis at weight `k - 12`
    rw [rank_eq_one_add_rank_cuspForm (by lia) hk2, CuspForm.discriminantEquiv.rank_eq,
      show ((k : ℤ) - 12 : ℤ) = ((k - 12 : ℕ) : ℤ) by lia,
      ihn (k - 12) (by lia) (by grind)]
    simp only [Nat.ModEq, show k / 12 = (k - 12) / 12 + 1 by lia,
      show (k - 12) % 12 = k % 12 by lia]
    split_ifs <;> grind

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

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

Tactic:
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.ModularForms.LevelOne.DimensionFormula

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

pp: case inr
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : 0 ≤ k
⊢ f = 0

Tactic:
· exact rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero hk) f

Goal state after:
case inr
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : 0 ≤ k
⊢ f = 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
y : ℝ
z : ℂ
hz : 0 < z.im
h : { coe := z, coe_im_pos := hz } ∈ truncatedFundamentalDomain y
⊢ ↑{ coe := z, coe_im_pos := hz } ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
exact ⟨hz.le, h.2, h.1.2, by simpa [Complex.normSq_eq_norm_sq] using h.1.1⟩

Goal state after:
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✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsBoundedAtImInfty ((SlashInvariantForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
SlashInvariantForm.trace,

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsBoundedAtImInfty
    ({
          toFun :=
            have this := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
            ∑ q, quotientFunc f q,
          slash_action_eq' := ⋯ }.toFun ∣[k]
      γ)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
⊢ Continuous[Pi.topologicalSpace, inst✝¹] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)

Tactic:
refine ⟨by fun_prop, fun H ↦ ?_⟩

Goal state after:
ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
⊢ Continuous[Pi.topologicalSpace, inst✝¹] f
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2.refine_1.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : InfinitePlace K
hw : w.IsComplex
⊢ (normAtPlace w) a = normAtComplexPlaces a w

Tactic:
normAtPlace_apply_of_isComplex hw,

Goal state after:
case refine_2.refine_1.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : InfinitePlace K
hw : w.IsComplex
⊢ ‖a.2 ⟨w, hw⟩‖ = normAtComplexPlaces a w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ y, ((mixedEmbedding K).toIntAlgHom.toLinearMap ∘ₗ ↑ℤ (↑↑↑J).subtype) y = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x

Tactic:
LinearMap.coe_comp,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ y, (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(↑ℤ (↑↑↑J).subtype)) y = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x
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
h : IsRamified K w
H : w.IsComplex ∧ (w.comap (algebraMap K L)).IsReal
⊢ Module.finrank v.Completion w.Completion = 2

Tactic:
NumberField.InfinitePlace.LiesOver.comap_eq w v

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
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
⊢ Module.finrank v.Completion w.Completion = 2
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
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |(of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).det|

Tactic:
← det_reindex_self f.symm,

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
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |((reindex f.symm f.symm)
          (of fun i w ↦
            if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))).det|
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ Irreducible P

Tactic:
have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
  obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
  refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
  rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
  exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ

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)ˣ
⊢ regOfFamily u / regulator K = ↑(Subgroup.closure (Set.range u) ⊔ torsion K).index

Tactic:
by
  rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_div_regOfFamily (isMaxRank_fundSystem K)
    (by simp only [closure_fundSystem_sup_torsion_eq_top, le_top]),
    closure_fundSystem_sup_torsion_eq_top, Subgroup.relIndex_top_right]

Goal state after:
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))
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
this✝ : P ∈ 𝒑.primesOver (𝓞 K)
this : span {hζ.toInteger - 1} ∈ 𝒑.primesOver (𝓞 K)
⊢ P = span {hζ.toInteger - 1}

Tactic:
have := ncard_primesOver_of_prime_pow p k K

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))
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
this✝¹ : P ∈ 𝒑.primesOver (𝓞 K)
this✝ : span {hζ.toInteger - 1} ∈ 𝒑.primesOver (𝓞 K)
this : (𝒑.primesOver (𝓞 K)).ncard = 1
⊢ P = span {hζ.toInteger - 1}
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ∀ (δ : ℝ), ¬HasDirichletDensity S δ
⊢ (if h : ∃ δ, HasDirichletDensity S δ then h.choose else 0) = 0

Tactic:
dif_neg (not_exists.mpr h)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ∀ (δ : ℝ), ¬HasDirichletDensity S δ
⊢ 0 = 0
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_5
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
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    2 ^ nrRealPlaces K * (↑NNReal.pi).toReal ^ nrComplexPlaces K * (ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)

Tactic:
ENNReal.coe_toReal,

Goal state after:
case e'_5
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
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * (ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ c K

Tactic:
rw [c]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ ↑(finrank ℚ K) * ‖(basisMatrix K)ᵀ⁻¹‖
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ Nat.Prime p

Tactic:
by
  have hp2 : 2 ≤ p := by
    by_contra! hp
    interval_cases p <;> grind
  rw [Nat.prime_iff_not_exists_mul_eq]
  refine ⟨hp2, ?_⟩
  rintro ⟨a, b, ha, hb, rfl⟩
  obtain ⟨ha₀, hb₀⟩ := mul_ne_zero_iff.mp (by omega : a * b ≠ 0)
  have h {n : ℕ} (hn₀ : n ≠ 0) (hn : n < a * b) : 1 ≤ f n := by
    by_contra! hn₁
    exact (not_le_of_gt hn) <| hmin n ⟨map_pos_of_ne_zero f (mod_cast hn₀), hn₁⟩
  rw [Nat.cast_mul, map_mul] at hp1
  exact not_le_of_gt hp1 <| one_le_mul_of_one_le_of_one_le (h ha₀ ha) (h hb₀ hb)

Goal state after:
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:
convert!
    Filter.Tendsto.congr' ?_
      (tendsto_finsetSum Finset.univ (fun C _ ↦ tendsto_norm_le_and_mk_eq_div_atTop K C))

Goal state after:
case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
      (↑(torsionOrder K) * √|↑(discr K)|) =
    ∑ c, 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|)

case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (fun b ↦ ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ b ∧ ClassGroup.mk0 I = c }) / b) =ᶠ[atTop] fun s ↦
    ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case hr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A

Tactic:
· exact mul_nonneg (c₂_nonneg _) Apos

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case pos
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
exact .inr <| equiv_padic_of_bounded hf_nontriv bdd

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

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℤ_[p] E
inst✝ : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
⊢ ‖mahlerTerm a n‖ ≤ ‖a‖

Tactic:
rw [ContinuousMap.norm_le_of_nonempty]

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℤ_[p] E
inst✝ : IsBoundedSMul ℤ_[p] E
a : E
n : ℕ
⊢ ∀ (x : ℤ_[p]), ‖(mahlerTerm a n) x‖ ≤ ‖a‖
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ x✝ ∈ HeightOneSpectrum.adicCompletionIntegers ℚ v ↔
    (HeightOneSpectrum.adicCompletion.equiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
by rw [HeightOneSpectrum.mem_adicCompletionIntegers]; rfl

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ x✝ ∈ HeightOneSpectrum.adicCompletionIntegers ℚ v ↔
    (HeightOneSpectrum.adicCompletion.uniformEquiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
by rw [HeightOneSpectrum.mem_adicCompletionIntegers]; rfl

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |(↑d * ↑q.den ^ 2 - ↑q.num ^ 2) / ↑q.den ^ 2| < ↑M / |↑q.den ^ 2|

Tactic:
abs_sq,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |(↑d * ↑q.den ^ 2 - ↑q.num ^ 2) / ↑q.den ^ 2| < ↑M / ↑q.den ^ 2