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

Goal state before:
pp: case «0».«0»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [ModularGroup.S]

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

Goal state before:
pp: case «0».«1»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [ModularGroup.S]

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

Goal state before:
pp: case «1».«0»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [ModularGroup.S]

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

Goal state before:
pp: case «1».«1»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [ModularGroup.S]

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

Tactic:
rintro rfl
    simp_rw [ModularForm.toFun_eq_coe, ModularForm.coe_trace, IsZeroAtImInfty, Filter.ZeroAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]
    let := Fintype.ofFinite 𝒬
    rw [show (0 : ℂ) = ∑ c : ℋ ⧸ 𝒢.subgroupOf ℋ, 0 by simp]
    refine tendsto_finsetSum _ (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ ?_)
    refine (translate f _).zero_at_cusps' ?_ γ rfl
    simpa using h.of_isFiniteRelIndex_conj hr

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: v : InfinitePlace ℚ
x : ℚ
⊢ ‖{ toCompletion := ↑((WithAbs.equiv ↑v).symm x) }‖ = ↑|(WithAbs.equiv ↑v) ((WithAbs.equiv ↑v).symm x)|

Tactic:
norm_coe,

Goal state after:
v : InfinitePlace ℚ
x : ℚ
⊢ v ((WithAbs.equiv ↑v) ((WithAbs.equiv ↑v).symm x)) = ↑|(WithAbs.equiv ↑v) ((WithAbs.equiv ↑v).symm x)|
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 * (QuotientGroup.mk' (torsion K)).range.index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0

Tactic:
QuotientGroup.range_mk',

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 * ⊤.index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * mixedEmbedding.norm x) *
          (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)

Tactic:
norm_eq_norm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑ζ)| * mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet
    (logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))

Tactic:
unfold logMap

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet
    ((fun x w ↦
        ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(Module.finrank ℚ K))⁻¹)) ⁻¹'
      ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
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)ˣ
hu : IsMaxRank u
⊢ regOfFamily u = ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))) volume

Tactic:
rw [regOfFamily, dif_pos hu]

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
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ u • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
simp [hx]

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
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : Nat.card Gal(K/↥K⁺) = 2
⊢ σ = τ

Tactic:
rw [Nat.card_eq_two_iff' 1] at this

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : ∃! y, y ≠ 1
⊢ σ = τ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
hx : (mixedEmbedding K) ↑x ∈ integerSet K
⊢ ↑(preimageOfMemIntegerSet ⟨(mixedEmbedding K) ↑x, hx⟩) = x

Tactic:
by
  simp_rw [RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    mixedEmbedding_preimageOfMemIntegerSet]

Goal state after:
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 : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ volume A =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
volume_eq_two_pow_mul_volume_plusPart hA₁ hm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ 2 ^ nrRealPlaces K * volume (plusPart A) =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)
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
⊢ regOfFamily (realFundSystem K) = |∏ w, 2| * regulator ↥K⁺

Tactic:
regulator_eq_regOfFamily_fundSystem,

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
⊢ regOfFamily (realFundSystem K) = |∏ w, 2| * regOfFamily (fundSystem ↥K⁺)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² : ℝ
x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ (x✝² • x✝¹) ↑x✝ - (↑(↑x✝).mult * ∑ w', (x✝² • x✝¹) w') * (↑(finrank ℚ K))⁻¹ =
    ((RingHom.id ℝ) x✝² • fun w ↦ x✝¹ ↑w - (↑(↑w).mult * ∑ w', x✝¹ w') * (↑(finrank ℚ K))⁻¹) x✝

Tactic:
simp [← mul_sum]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² : ℝ
x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² * x✝¹ ↑x✝ - ↑(↑x✝).mult * (x✝² * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹ =
    x✝² * (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
⊢ Real.exp ((↑x✝.mult)⁻¹ * (completeBasis K) w₀ x✝) = Real.exp 1

Tactic:
completeBasis_apply_of_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
⊢ Real.exp ((↑x✝.mult)⁻¹ * ↑x✝.mult) = Real.exp 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ |((LinearMap.toMatrix (completeBasis K) (completeBasis K)) ↑↑(completeBasis K).equivFunL.symm).transpose.det| =
    ↑(finrank ℚ K) * regulator K

Tactic:
regulator_eq_regOfFamily_fundSystem,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ |((LinearMap.toMatrix (completeBasis K) (completeBasis K)) ↑↑(completeBasis K).equivFunL.symm).transpose.det| =
    ↑(finrank ℚ K) * regOfFamily (fundSystem K)
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 φ σ
⊢ ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ

Tactic:
intro ψ

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 φ σ
ψ : K →+* ℂ
⊢ ComplexEmbedding.IsConj ψ σ
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ regulator K = |(Matrix.of fun i ↦ (logEmbedding K) (Additive.ofMul (fundSystem K ((equivFinRank K).symm i)))).det|

Tactic:
regulator_eq_regOfFamily_fundSystem,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ regOfFamily (fundSystem K) =
    |(Matrix.of fun i ↦ (logEmbedding K) (Additive.ofMul (fundSystem K ((equivFinRank K).symm i)))).det|
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ regulator K = |(Matrix.of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|

Tactic:
regulator_eq_regOfFamily_fundSystem,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ regOfFamily (fundSystem K) =
    |(Matrix.of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regulator K =
    |(Matrix.of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

Tactic:
regulator_eq_regOfFamily_fundSystem,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regOfFamily (fundSystem K) =
    |(Matrix.of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|
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:
regulator_eq_regOfFamily_fundSystem,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ regOfFamily u / regOfFamily (fundSystem K) = ↑(Subgroup.closure (Set.range u) ⊔ torsion K).index
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (↑expMapBasis '' Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1).Nonempty

Tactic:
exact Set.image_nonempty.mpr (Set.univ_pi_nonempty_iff.mpr (by aesop))

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
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
by
  have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
  have h_main := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝒑 (𝓞 K) Gal(K/ℚ)
  have hζ := hK.zeta_spec
  have := liesOver_span_zeta_sub_one p k hζ
  rwa [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hζ.toInteger - 1}) Gal(K/ℚ),
    inertiaDegIn_eq_inertiaDeg 𝒑 (span {hζ.toInteger - 1}) Gal(K/ℚ),
    inertiaDeg_span_zeta_sub_one,
    ramificationIdx_span_zeta_sub_one, mul_one, ← Nat.totient_prime_pow_succ hp.out,
    ← finrank _ K, IsGaloisGroup.card_eq_finrank Gal(K/ℚ) ℚ K, Nat.mul_eq_right] at h_main
  exact Module.finrank_pos.ne'

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p - 1

Tactic:
by
  rw [← pow_one p] at hK hζ
  rw [ramificationIdx_span_zeta_sub_one p 0 hζ, pow_zero, one_mul]

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 = ↑(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) σ

Tactic:
Nat.cast_pow,

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.Cyclotomic.Ideal

Goal state before:
pp: case hsep
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)).Separable

Tactic:
exact (zeta_spec m ℚ K).toInteger_isPrimitiveRoot.separable_minpoly_mod hm

Goal state after:
Module: Mathlib.RingTheory.Unramified.Dedekind

Goal state before:
pp: case hIq
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this✝¹ : p.IsMaximal
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing (B ⧸ Ideal.map (algebraMap A B) p)
⊢ q ∈ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) '' minimalPrimes (B ⧸ Ideal.map (algebraMap A B) p)

Tactic:
exact ⟨q.map (Ideal.Quotient.mk (p.map (algebraMap A B))),
      IsArtinianRing.mem_minimalPrimes bot_le, Ideal.comap_map_mk Ideal.map_comap_le⟩

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
⊢ ‖x - y‖ ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
rw [← norm_replicateCol (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
⊢ ∀ (i : β) (j : Unit), ‖replicateCol Unit (x - y) i j‖ ≤ (↑n * max 1 ‖A‖) ^ e
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ f ↑n = f ↑(n ^ k) ^ (↑k)⁻¹

Tactic:
Nat.cast_pow,

Goal state after:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ f ↑n = f (↑n ^ k) ^ (↑k)⁻¹
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (logb ↑n₀ ↑(n ^ k) + 1)) ^ (↑k)⁻¹ = (↑n₀ * (↑k * logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹

Tactic:
Nat.cast_pow,

Goal state after:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (logb (↑n₀) (↑n ^ k) + 1)) ^ (↑k)⁻¹ = (↑n₀ * (↑k * logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ 0 ≤ y i

Tactic:
exact hyT.1 i

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
he : 0 < ↑m * f ↑m / (f ↑m - 1)
⊢ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑(n ^ k) = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ (↑k * logb ↑m ↑n)

Tactic:
Nat.cast_pow,

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
he : 0 < ↑m * f ↑m / (f ↑m - 1)
⊢ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb (↑m) (↑n ^ k) = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ (↑k * logb ↑m ↑n)