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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ atImInfty.ZeroAtFilter fun τ ↦ ‖petersson k (⇑f) (⇑f') (g • τ)‖

Tactic:
ZeroAtFilter,

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ Tendsto (fun τ ↦ ‖petersson k (⇑f) (⇑f') (g • τ)‖) atImInfty (𝓝 0)
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
hk' : 2 < ↑k
⊢ ∑' (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)

Tactic:
apply (summable_norm_eisSummand hk _).tsum_le_tsum _

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
hk' : 2 < ↑k
⊢ Summable fun i ↦ r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖i‖ ^ (-k)

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
hk' : 2 < ↑k
⊢ ∀ (i : Fin 2 → ℤ),
    ‖eisSummand k i (ModularGroup.T ^ (↑N * n) • z)‖ ≤
      r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖i‖ ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ atImInfty.ZeroAtFilter ⇑f

Tactic:
ZeroAtFilter,

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ Tendsto (⇑f) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℂ
n : ℕ
⊢ logDeriv (fun x ↦ 1 - eta_q n x) z = 2 * ↑π * I * (↑n + 1) * -eta_q n z / (1 - eta_q n z)

Tactic:
by
  have h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (n + 1) * x)) =
      ((fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (n + 1) * x) := by aesop
  simp_rw [eta_q_eq_cexp, h2, logDeriv_one_sub_mul_cexp_comp 1
    (g := fun x ↦ (2 * π * I * (n + 1) * x)) (by fun_prop), deriv_const_mul_id]
  simp

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

Goal state before:
pp: z : ℍ
⊢ Summable fun m ↦ ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1))⁻¹ + δ m - δ m

Tactic:
add_sub_cancel_right

Goal state after:
z : ℍ
⊢ Summable fun m ↦ ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1))⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
this : D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) = -D2 g⁻¹
⊢ G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) + D2 g⁻¹ - D2 g⁻¹

Tactic:
add_sub_cancel_right

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
this : D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) = -D2 g⁻¹
⊢ G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
c : ℂ := (2 * ↑π * I)⁻¹
⊢ DifferentiableOn ℂ (D F ∘ ↑ofComplex) {z | 0 < z.im}

Tactic:
have hDeriv : DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ofComplex) z) upperHalfPlaneSet := by
    simpa [c] using (hF.deriv isOpen_upperHalfPlaneSet).const_mul ((2 * π * I)⁻¹)

Goal state after:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
c : ℂ := (2 * ↑π * I)⁻¹
hDeriv : DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ↑ofComplex) z) upperHalfPlaneSet
⊢ DifferentiableOn ℂ (D F ∘ ↑ofComplex) {z | 0 < z.im}
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
this : η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
⊢ Δ { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } *
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z ^
        (-12) =
    Δ z

Tactic:
simpa [denom, ModularGroup.S]

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z

Tactic:
iteratedDerivWithin_const_sub hk,

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun z ↦ -(2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n)) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

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

Tactic:
have hqc4 : c4 • qExpansion 1 (E₄ : ℍ → ℂ) = qExpansion 1 (f : ℍ → ℂ) ^ 2 := by
    rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
      show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]

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

Goal state before:
pp: case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y

Tactic:
· rintro ⟨hz, h1, h2, h3⟩
    have hz' : 0 < z.im := by
      apply hz.lt_of_ne
      contrapose! h3
      simpa [← sq_lt_one_iff₀ (norm_nonneg _), ← Complex.normSq_eq_norm_sq, Complex.normSq,
        ← h3, ← sq] using h2.trans_lt (by norm_num)
    exact ⟨⟨z, hz'⟩, ⟨⟨by simpa [Complex.normSq_eq_norm_sq], h2⟩, h1⟩, rfl⟩

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✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsZeroAtImInfty ((ModularForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
simp_rw [ModularForm.toFun_eq_coe, ModularForm.coe_trace, IsZeroAtImInfty, Filter.ZeroAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 0)
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)
S : Set ι
⊢ TopologicalSpace.induced DFunLike.coe inferInstance ≤
    TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced DFunLike.coe inferInstance)

Tactic:
rw [inclusion_eq_id R A (𝓟 S), @coinduced_id]

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
⊢ x ^ n - y ^ n ≠ 0

Tactic:
· simp [← Nat.pos_iff_ne_zero, tsub_pos_iff_lt, Nat.pow_lt_pow_left hyx hn]

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

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

Tactic:
det_fderivPiPolarCoordSymm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
this : ↑(FDerivPolarCoordRealSymm K x) = LinearMap.id.prodMap ↑(fderivPiPolarCoordSymm x.2)
⊢ ∏ i, (x.2 i).1 = ∏ w, (x.2 w).1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
e : logSpace K
h₁ : e ∈ Submodule.span ℤ (Set.range ⇑B)
h₂ : ⟨e, h₁⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
exact ⟨⟨e, by rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
⊢ ∃ u, u • x ∈ fundamentalCone K

Tactic:
let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B
  · exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩
  · obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)
    exact ⟨⟨e, by rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩

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

Goal state before:
pp: case refine_2.refine_1.inl
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.IsReal
⊢ normAtAllPlaces a w = normAtComplexPlaces a w

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
⊢ normAtAllPlaces a w = normAtComplexPlaces a w

Tactic:
· simpa [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, normAtPlace_apply_of_isReal hw]
          using (ha₂ ⟨w, hw⟩).le

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
⊢ normAtAllPlaces a w = normAtComplexPlaces a w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : realSpace K
x✝ : InfinitePlace K
⊢ ↑expMap (x + y) x✝ = (↑expMap x * ↑expMap y) x✝

Tactic:
simp [mul_add, Real.exp_add]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ (Matrix.of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(realFundSystem K (g.symm i))))).submatrix
      ⇑f.symm ⇑f.symm =
    Matrix.of fun i j ↦
      2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i j

Tactic:
ext i w

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ (Matrix.of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(realFundSystem K (g.symm i))))).submatrix
      (⇑f.symm) (⇑f.symm) i w =
    Matrix.of
      (fun i j ↦
        2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i j)
      i w
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hj : j.Coprime n
u : Aˣ
hu : (ζ ^ 1 - 1) * ↑u = ζ ^ j - 1
⊢ 1 - ζ ≠ 0

Tactic:
grind [sub_one_ne_zero]

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

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ hζ.toInteger - 1 ≠ 0

Tactic:
· exact Prime.ne_zero hζ.zeta_sub_one_prime

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
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsMulCommutative Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
⊢ Nat.card ↥(OrderDual.ofDual ((subgroupGalEquivSubgroupChar n K R) H)) = Nat.card (Gal(K/ℚ) ⧸ H)

Tactic:
subgroupGalEquivSubgroupChar,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsMulCommutative Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
⊢ Nat.card ↥(OrderDual.ofDual (((galEquivZMod n K).mapSubgroup.trans (subgroupOrderIsoSubgroupMulChar (ZMod n) R)) H)) =
    Nat.card (Gal(K/ℚ) ⧸ H)
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
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝³ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ σ ∈ F.fixingSubgroup, χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ (a : Gal(K/ℚ)), (∀ x ∈ F, a x = x) → (toUnitHom χ) ((galEquivZMod n K) a) = 1

Tactic:
IntermediateField.mem_fixingSubgroup_iff,

Goal state after:
n : ℕ
inst✝⁸ : NeZero n
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝³ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ (σ : Gal(K/ℚ)), (∀ x ∈ F, σ x = x) → χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ (a : Gal(K/ℚ)), (∀ x ∈ F, a x = x) → (toUnitHom χ) ((galEquivZMod n K) a) = 1
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:
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.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
    ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
← inverse_basisMatrix_mulVec_eq_repr

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun j ↦ (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i‖ ≤
    ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖
Module: Mathlib.NumberTheory.SiegelsLemma

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

Tactic:
negPart_eq_neg.2 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
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]) n, coe_eq]

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: case refine_3
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
⊢ x ∈ ⋃ j, ↑((fun k ↦ W ↑(t.equivFin.symm k)) j)

Tactic:
obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩

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

Goal state before:
pp: case refine_2
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[↑(primesEquiv v)]
hy : y ∈ ↑(subring ↑(primesEquiv v))
⊢ y ∈ ⇑(padicEquiv v) '' ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)

Tactic:
obtain ⟨x, hx⟩ := (adicCompletionIntegers.padicIntEquiv v).surjective ⟨y, hy⟩

Goal state after:
case refine_2
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[↑(primesEquiv v)]
hy : y ∈ ↑(subring ↑(primesEquiv v))
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
hx : (adicCompletionIntegers.padicIntEquiv v) x = ⟨y, hy⟩
⊢ y ∈ ⇑(padicEquiv v) '' ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: case e_6
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
y : Y
⊢ μ { toFun := fun x ↦ (f.comp fst * g.comp snd) (x, y), continuous_toFun := ⋯ } = μ f * g y

Tactic:
mul_comm (μ f) (g y),

Goal state after:
case e_6
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
y : Y
⊢ μ { toFun := fun x ↦ (f.comp fst * g.comp snd) (x, y), continuous_toFun := ⋯ } = g y * μ f
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²¹ : Field K
inst✝²⁰ : Field L
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.LiesOver p
inst✝¹⁴ : FiniteDimensional K L
inst✝¹³ : MulSemiringAction Gal(L/K) B
inst✝¹² : IsGaloisGroup Gal(L/K) A B
inst✝¹¹ : IsDedekindDomain A
inst✝¹⁰ : IsDedekindDomain B
inst✝⁹ : Module.Finite A B
inst✝⁸ : Module.IsTorsionFree A B
inst✝⁷ : Ring.HasFiniteQuotients A
inst✝⁶ : P.IsMaximal
D : Type u_5
inst✝⁵ : Field D
inst✝⁴ : Algebra D L
inst✝³ : IsDecompositionField K L P D
inst✝² : IsGalois K L
inst✝¹ : Algebra K D
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : FiniteDimensional D L
⊢ Module.finrank K D * Module.finrank D L = (p.primesOver B).ncard * Module.finrank D L

Tactic:
Module.finrank_mul_finrank,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²¹ : Field K
inst✝²⁰ : Field L
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.LiesOver p
inst✝¹⁴ : FiniteDimensional K L
inst✝¹³ : MulSemiringAction Gal(L/K) B
inst✝¹² : IsGaloisGroup Gal(L/K) A B
inst✝¹¹ : IsDedekindDomain A
inst✝¹⁰ : IsDedekindDomain B
inst✝⁹ : Module.Finite A B
inst✝⁸ : Module.IsTorsionFree A B
inst✝⁷ : Ring.HasFiniteQuotients A
inst✝⁶ : P.IsMaximal
D : Type u_5
inst✝⁵ : Field D
inst✝⁴ : Algebra D L
inst✝³ : IsDecompositionField K L P D
inst✝² : IsGalois K L
inst✝¹ : Algebra K D
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : FiniteDimensional D L
⊢ Module.finrank K L = (p.primesOver B).ncard * Module.finrank D L