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

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ C * (1 / τ.im ^ k) = C * ‖(τ.im ^ k)⁻¹‖

pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 1 ≤ 1 / τ.im ^ k

Tactic:
Real.norm_of_nonneg (by positivity),

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ C * (1 / τ.im ^ k) = C * (τ.im ^ k)⁻¹

k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 1 ≤ 1 / τ.im ^ k
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
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
τ : ℍ
⊢ C / τ.im ^ (↑k / 2) = C * ‖τ.im ^ (-(↑k / 2))‖

Tactic:
Real.norm_of_nonneg (by positivity),

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
τ : ℍ
⊢ C / τ.im ^ (↑k / 2) = C * τ.im ^ (-(↑k / 2))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at this

Goal state after:
z : ℍ
this : Summable (G2Term z ∘ ⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm)
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: γ : SL(2, ℤ)
⊢ γ ∈ Subgroup.closure {S, T}

Tactic:
simp [SpecialLinearGroup.SL2Z_generators]

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

Goal state before:
pp: z : ℍ
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = logDeriv (sqrt * η) ↑z

Tactic:
Pi.mul_def,

Goal state after:
z : ℍ
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = logDeriv (fun i ↦ i.sqrt * η i) ↑z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl.inl
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hnm : ‖↑z‖ = 1
hg : S • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑S 1 0
hc : ↑S 1 0 = 1
hd : ↑S 1 1 = 0
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑z) = 1

pp: case inr.inl.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T⁻¹ * S) 1 0
hc : ↑(T⁻¹ * S) 1 0 = 1
hd : ↑(T⁻¹ * S) 1 1 = 0
hz : ρ ∈ 𝒟
hg : (T⁻¹ * S) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S))) ↑ρ) = 1

pp: case inr.inl.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S) 1 0
hc : ↑(T * S) 1 0 = 1
hd : ↑(T * S) 1 1 = 0
hz : 1 +ᵥ ρ ∈ 𝒟
hg : (T * S) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S))) ↑(1 +ᵥ ρ)) = 1

Tactic:
· simp [normSq_eq_norm_sq, denom, coe_S, hnm]

Goal state after:
case inr.inl.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T⁻¹ * S) 1 0
hc : ↑(T⁻¹ * S) 1 0 = 1
hd : ↑(T⁻¹ * S) 1 1 = 0
hz : ρ ∈ 𝒟
hg : (T⁻¹ * S) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S))) ↑ρ) = 1

case inr.inl.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S) 1 0
hc : ↑(T * S) 1 0 = 1
hd : ↑(T * S) 1 1 = 0
hz : 1 +ᵥ ρ ∈ 𝒟
hg : (T * S) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S))) ↑(1 +ᵥ ρ)) = 1
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inl
k : ℕ
hk_even : Even ↑k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) < Cardinal.aleph0

Tactic:
rw [dimension_level_one k (mod_cast hk_even)]

Goal state after:
case inr.inl
k : ℕ
hk_even : Even ↑k
⊢ ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) < Cardinal.aleph0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case refine_2
⊢ IsClosed fun z ↦ Real.le✝ 1 ‖z‖

Tactic:
exact isClosed_le continuous_const continuous_norm

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.refine_1
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun x_1 ↦ ‖↑(↑ofComplex (↑x_1 * ↑x))‖) (𝓝 1) (𝓝 ‖↑x‖)

pp: case h.refine_2
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |(↑ofComplex (↑x_1 * ↑x)).re| < 1 / 2

Tactic:
· have : ContinuousAt (fun a : ℝ ↦ (ofComplex (a * x : ℂ) : ℂ)) 1 := by
        refine .comp (by fun_prop) ((OpenPartialHomeomorph.continuousAt _ ?_).comp (by fun_prop))
        simpa [ofComplex] using x.coe_im_pos
      simpa [ofComplex_apply_of_im_pos x.coe_im_pos] using this.tendsto.norm

Goal state after:
case h.refine_2
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |(↑ofComplex (↑x_1 * ↑x)).re| < 1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ

Tactic:
← closure_closure

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure (closure 𝒟ᵒ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
t : ℝ≥0
⊢ 0 < (↑x + ↑↑t * Complex.I).im

Tactic:
simpa using! add_pos_of_pos_of_nonneg x.coe_im_pos t.property

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
y : ℝ
⊢ IsClosed fun z ↦ Real.le✝ 1 ‖z‖

Tactic:
exact isClosed_le continuous_const continuous_norm

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

Goal state before:
pp: case refine_2
Γ : 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
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
⊢ (fun i ↦ ‖(PowerSeries.coeff i) (qExpansion (h Γ) ⇑f)‖ / ↑i ^ s.re) =O[atTop] fun n ↦ ↑n ^ (r - s.re)

Tactic:
simp only [Real.rpow_sub' (Nat.cast_nonneg _) (show r - s.re ≠ 0 by linarith)]

Goal state after:
case refine_2
Γ : 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
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
⊢ (fun i ↦ ‖(PowerSeries.coeff i) (qExpansion (h Γ) ⇑f)‖ / ↑i ^ s.re) =O[atTop] fun n ↦ ↑n ^ r / ↑n ^ s.re
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
⊢ x - y ≠ 0

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

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

Tactic:
· exact Nat.sub_ne_zero_of_lt hyx

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

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

Goal state before:
pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x - y ≠ 0

pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x ^ n - y ^ n ≠ 0

Tactic:
· exact Nat.sub_ne_zero_of_lt hyx

Goal state after:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x ^ n - y ^ n ≠ 0
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)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (AddSubgroup.closure (⇑Additive.toMul ⁻¹' QuotientGroup.mk '' Set.range u))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0

Tactic:
← Equiv.image_symm_eq_preimage

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0
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
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ ComplexEmbedding.IsConj (φ.comp ↑ν.symm) σ

Tactic:
rw [show σ = ν.symm⁻¹ * σ * ν.symm by simp]

Goal state after:
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
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ ComplexEmbedding.IsConj (φ.comp ↑ν.symm) (ν.symm⁻¹ * σ * ν.symm)
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 =
    |∑ j,
          (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⟩)))))
            (f.symm w') j| *
      |(((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⟩)))))).submatrix
            (f.symm w').succAbove (f.symm w').succAbove).det|

Tactic:
simp_rw [reindex_apply, submatrix_submatrix, ← f.symm.sum_comp, f.symm_symm, submatrix_apply,
      Function.comp_def, Equiv.apply_symm_apply, of_apply, dif_pos, ← Nat.cast_sum, sum_mult_eq,
      Nat.abs_cast]
    rw [regOfFamily_eq_det u w' e, ← Matrix.det_reindex_self g]
    congr with i j
    rw [reindex_apply, submatrix_apply, submatrix_apply, of_apply, of_apply, dif_neg]
    rfl

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
⊢ (fun i ↦ Real.exp (x w₀)) * ↑expMap (∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
Pi.mul_def,

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

Goal state before:
pp: n✝ j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hj (by lia)

Goal state after:
n✝ j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
m : ℕ
hm : j * m % (n + 2) = 1
⊢ ζ ^ j - 1 ∣ ζ - 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this : (↑((galEquivZMod m F) (σ.restrictNormal F))).val % m = (↑((galEquivZMod n K) σ)).val % m
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)

Tactic:
← ZMod.natCast_eq_natCast_iff',

Goal state after:
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this : ↑(↑((galEquivZMod m F) (σ.restrictNormal F))).val = ↑(↑((galEquivZMod n K) σ)).val
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ (∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp (xᵢ * ↑n))) *
      ∏ i, (volume.restrict (if ↑i = w₀ then Set.Iic 0 else Set.Ico 0 1)) Set.univ =
    (↑n)⁻¹

Tactic:
if_neg
    (Finset.ne_of_mem_erase (Subtype.prop _)),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ (∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp (xᵢ * ↑n))) * ∏ x, (volume.restrict (Set.Ico 0 1)) Set.univ =
    (↑n)⁻¹
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
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
rw [← pow_one p] at hK
  exact ncard_primesOver_of_prime_pow p 0 K

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : (↑((galEquivZMod n K) σ)).val % n = p ^ i % n
h₀ : IsPrimitiveRoot ((Ideal.Quotient.mk P) hζ.toInteger) n
h₁ :
  ((IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩)
      ((Ideal.Quotient.mk P) hζ.toInteger) =
    (Ideal.Quotient.mk P) (σ • hζ.toInteger)
⊢ (fun x ↦ ZMod.unitOfCoprime p hn ^ x) ↑i = (galEquivZMod n K) σ

Tactic:
← ZMod.natCast_eq_natCast_iff',

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ↑(↑((galEquivZMod n K) σ)).val = ↑(p ^ i)
h₀ : IsPrimitiveRoot ((Ideal.Quotient.mk P) hζ.toInteger) n
h₁ :
  ((IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩)
      ((Ideal.Quotient.mk P) hζ.toInteger) =
    (Ideal.Quotient.mk P) (σ • hζ.toInteger)
⊢ (fun x ↦ ZMod.unitOfCoprime p hn ^ x) ↑i = (galEquivZMod n K) σ
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ 0 ≤ dirichletDensity S

Tactic:
dirichletDensity

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ 0 ≤ if h : ∃ δ, HasDirichletDensity S δ then h.choose else 0
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ dirichletDensity S ≤ 1

Tactic:
dirichletDensity

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ (if h : ∃ δ, HasDirichletDensity S δ then h.choose else 0) ≤ 1
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case hbc
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := ⋯
j : K →+* ℂ
a✝ : j ∈ univ
⊢ ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤ house ((algebraMap (𝓞 K) K) α)

Tactic:
exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

pp: case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

pp: case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

pp: case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
· rw [negPart_eq_zero.2 hsign]
    exact mul_nonneg (hv.1 j) hsign

Goal state after:
case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ 0 ≤ P i + 1

Tactic:
apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ ∀ i_1 ∈ univ, 0 ≤ ↑B * (A i i_1)⁺
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_4
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
⊢ MeasureTheory.volume (frontier (⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1})) = 0

Tactic:
← (toMixed K).coe_toHomeomorph,

Goal state after:
case convert_4
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
⊢ MeasureTheory.volume
      (frontier (⇑(toMixed K).toHomeomorph ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1})) =
    0
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

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

Tactic:
filter_upwards [eventually_ge_atTop 0] with s hs

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
⊢ ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = c }) / s = ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

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

Tactic:
filter_upwards [eventually_ge_atTop 0] with s hs

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this :
  Tendsto (fun x ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ x }) / x + x⁻¹) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))
s : ℝ
hs : 0 ≤ s
⊢ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s + s⁻¹ = ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s