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

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)

Tactic:
intro n

Goal state after:
τ : ℂ
hτ : 0 < τ.im
n : ℕ
⊢ ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∀ (i : ℕ), ‖↑((σ (k - 1)) i) * cexp (2 * ↑π * I * ↑z) ^ i‖ ≤ ‖↑i ^ k * cexp (2 * ↑π * I * ↑z) ^ i‖

Tactic:
intro n

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ ‖↑((σ (k - 1)) n) * cexp (2 * ↑π * I * ↑z) ^ n‖ ≤ ‖↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℕ
⊢ ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)

Tactic:
simpa only [Int.cast_add, Int.cast_one] using! norm_exp_mul_sq_le hτ (n + 1)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
⊢ IsCompact (truncatedFundamentalDomain y)

Tactic:
isEmbedding_coe.isCompact_iff,

Goal state after:
y : ℝ
⊢ IsCompact (UpperHalfPlane.coe '' truncatedFundamentalDomain y)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ^ 2 ∣ ↑p * y ^ (p - 1)

Tactic:
pow_two,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p * ↑p ∣ ↑p * y ^ (p - 1)
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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
⊢ ↑(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) ⊆ ↑(unitLattice K)

Tactic:
rw [SetLike.coe_subset_coe, Submodule.span_le]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
⊢ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))) ⊆ ↑(unitLattice K)
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
c : ℝ
hc : c ≠ 0
⊢ logMap (c • x) = logMap x

Tactic:
have : mixedEmbedding.norm (c • (1 : mixedSpace K)) ≠ 0 := by
    rw [norm_smul, map_one, mul_one]
    exact pow_ne_zero _ (abs_ne_zero.mpr hc)
  rw [← smul_one_mul, logMap_mul this hx, logMap_real, zero_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
⊢ Module.finrank ℚ ↥K⁺ * 2 = Module.finrank ℚ ↥K⁺ * Module.finrank (↥K⁺) K

Tactic:
IsQuadraticExtension.finrank_eq_two _ K

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ Module.finrank ℚ ↥K⁺ * 2 = Module.finrank ℚ ↥K⁺ * 2
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = ↑x
⊢ (algebraMap (↥K⁺) K) ((algebraMap (𝓞 ↥K⁺) ↥K⁺) y) ∈ K⁺

Tactic:
exact SetLike.coe_mem _

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

Goal state before:
pp: case e'_3
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 = (Subgroup.map (unitsMulComplexConjInv K) (torsion K)).index

Tactic:
rw [map_unitsMulComplexConjInv_torsion, IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right]
    exact even_iff_two_dvd.mp (even_torsionOrder K)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ logMap (mixedSpaceOfRealSpace (normAtAllPlaces x)) ∈
        ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      mixedSpaceOfRealSpace (normAtAllPlaces x) ∉ {x | mixedEmbedding.norm x = 0} ↔
    logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
logMap_normAtAllPlaces,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      mixedSpaceOfRealSpace (normAtAllPlaces x) ∉ {x | mixedEmbedding.norm x = 0} ↔
    logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      x ∉ {x | mixedEmbedding.norm x = 0}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ realSpaceToLogSpace (completeFamily K w₀) = 0

Tactic:
by
  ext
  rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]

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

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ x_1, Real.exp ((↑1)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1)) *
      ∏ x_1, Real.exp ((↑2)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1) =
    (∏ x_1, Real.exp ((↑1)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1)) *
        (∏ x_1, Real.exp ((↑2)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1)) ^ 2 *
      (∏ x_1, Real.exp ((↑2)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1))⁻¹

Tactic:
pow_two,

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ x_1, Real.exp ((↑1)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1)) *
      ∏ x_1, Real.exp ((↑2)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1) =
    (∏ x_1, Real.exp ((↑1)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1)) *
        ((∏ x_1, Real.exp ((↑2)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1)) *
          ∏ x_1, Real.exp ((↑2)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1)) *
      (∏ x_1, Real.exp ((↑2)⁻¹ * (completeBasis K).equivFun.symm x ↑x_1))⁻¹
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
⊢ IsUnit (∑ i ∈ range j, ζ ^ i)

Tactic:
obtain ⟨u, hu⟩ := hζ.associated_pow_sub_one_pow_of_coprime hj (coprime_one_left n)

Goal state after:
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
⊢ IsUnit (∑ i ∈ range j, ζ ^ i)
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))
⊢ (span {hζ.toInteger - 1}).IsPrime

Tactic:
rw [span_singleton_prime]

Goal state after:
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))
⊢ Prime (hζ.toInteger - 1)

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
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)) = (↑((galEquivZMod n K) σ)).cast
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)

Tactic:
Units.ext_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)) = (↑((galEquivZMod n K) σ)).cast
⊢ ↑((galEquivZMod m F) (σ.restrictNormal F)) = ↑((ZMod.unitsMap h) ((galEquivZMod n K) σ))
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))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 = span {hζ.toInteger - 1} ^ Module.finrank ℚ K

Tactic:
rw [map_span, Set.image_singleton, span_singleton_eq_span_singleton.mpr
    ((associated_norm_zeta_sub_one p k hζ).symm.map (algebraMap ℤ (𝓞 K))),
    ← Algebra.intNorm_eq_norm, Algebra.algebraMap_intNorm_of_isGalois, ← prod_span_singleton]

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))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
⊢ ∏ i, span {i (hζ.toInteger - 1)} = span {hζ.toInteger - 1} ^ Module.finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: 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.Coprime m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ : P.inertiaDeg ℤ = (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).natDegree
this : P.IsMaximal
⊢ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ) ∣ cyclotomic m (ZMod p)

Tactic:
← map_cyclotomic_int,

Goal state after:
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.Coprime m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ : P.inertiaDeg ℤ = (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).natDegree
this : P.IsMaximal
⊢ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (cyclotomic m ℤ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in closure (paramSet K),
          ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
            ∏ w, ENNReal.ofReal (↑expMapBasis x ↑w)) =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in interior (paramSet K),
          ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
            ∏ w, ENNReal.ofReal (↑expMapBasis x ↑w))

Tactic:
setLIntegral_congr (closure_paramSet_ae_interior K)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in interior (paramSet K),
          ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
            ∏ w, ENNReal.ofReal (↑expMapBasis x ↑w)) =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in interior (paramSet K),
          ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
            ∏ w, ENNReal.ofReal (↑expMapBasis x ↑w))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
· refine lt_top_iff_ne_top.mp <| lt_of_le_of_lt (measure_mono interior_subset) ?_
    rw [volume_normLeOne]
    exact Batteries.compareOfLessAndEq_eq_lt.mp rfl

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:
rw [subgroupGalEquivSubgroupChar, OrderIso.trans_apply, card_subgroupOrderIsoSubgroupMulChar]
  exact Nat.card_congr (QuotientGroup.congr _ _ (galEquivZMod n K) rfl).symm.toEquiv

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : 𝓞 K
hx₂ : x ∈ ↑J
hx₃ : mixedEmbedding.norm ((mixedEmbedding K) ↑x) ≤ s
hx₁ : (mixedEmbedding K) ↑x ∈ fundamentalCone K
⊢ ↑x ∈ ↑↑↑J

Tactic:
simp [hx₂]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
⊢ ∃ w, 1 ≤ w ↑α

Tactic:
by_contra! h_neg
    let w₀ := Classical.arbitrary (InfinitePlace K)
    have h_ge_one : 1 ≤ w₀ α := InfinitePlace.one_le_of_lt_one hα0 (fun z _ ↦ h_neg z)
    exact (h_neg w₀).not_ge h_ge_one

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

Goal state before:

Tactic:
_ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
    _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
    _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
        * house (algebraMap (𝓞 K) K α) := by
      gcongr with j
      exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
    _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
      simp [Embeddings.card, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case hz
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ 0 < ↑n - ↑m

Tactic:
exact sub_pos.mpr (mod_cast hn)

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia : (a, i) ∈ L.zipIdx
⊢ (⇑f ∘ Nat.cast ∘ fun x ↦ x.1 * m ^ x.2) (a, i) ≤ ↑m * f ↑m ^ (a, i).2

Tactic:
replace hia := List.mem_zipIdx hia

Goal state after:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = L[i - 0]
⊢ (⇑f ∘ Nat.cast ∘ fun x ↦ x.1 * m ^ x.2) (a, i) ≤ ↑m * f ↑m ^ (a, i).2
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
⊢ ∀ (n : ℕ), f ↑n ≤ 1

Tactic:
intro n

Goal state after:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
⊢ f ↑n ≤ 1
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)
⊢ f ↑n ^ k ≤ (↑m * f ↑m / (f ↑m - 1)) ^ 1 * f ↑m ^ (logb ↑m ↑n * ↑k)

Tactic:
rpow_one,

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)
⊢ f ↑n ^ k ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ (logb ↑m ↑n * ↑k)
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
δ : ℝ
hδp : δ > 0
hδ : ∀ ⦃x_1 : ℤ_[p]⦄, dist x_1 x < δ → dist (f x_1) (f x) < ‖↑k.factorial‖
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖

Tactic:
obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
δ : ℝ
hδp : δ > 0
hδ : ∀ ⦃x_1 : ℤ_[p]⦄, dist x_1 x < δ → dist (f x_1) (f x) < ‖↑k.factorial‖
n : ℕ
hn' : dist x ↑n < δ
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ ∀ (i : ℕ),
    ∃ j,
      ∀ (x y : WithVal (Rat.padicValuation p)),
        Valued.v.restrict (y - x) < ↑j → ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹

Tactic:
intro n

Goal state after:
case left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
⊢ ∃ j,
    ∀ (x y : WithVal (Rat.padicValuation p)),
      Valued.v.restrict (y - x) < ↑j → ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ n)⁻¹
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
t : ℕ
ht : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
t : ℕ
ht : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
m : ℕ
hm : s * p ^ t ≤ m
⊢ ‖Δ_[1]^[m] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ Tendsto (fun n ↦ mahlerTerm (a n) n) cofinite (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero] at ha ⊢

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto (fun x ↦ ‖a x‖) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ ‖mahlerTerm (a x) x‖) cofinite (𝓝 0)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ d * a.y ^ 2
⊢ False

Tactic:
a.prop_y,

Goal state after:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ a.x ^ 2 - 1
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < d * a.y ^ 2

Tactic:
a.prop_y,

Goal state after:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < a.x ^ 2 - 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ Int.ofNat n).x

Tactic:
| ofNat n =>

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ d * a.y ^ 2 = d * b.y ^ 2

Tactic:
a.prop_y,

Goal state after:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a.x ^ 2 - 1 = d * b.y ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
⊢ ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y

Tactic:
intro n

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: case inr
A : Type u_1
B : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : Module.IsTorsionFree A B
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ (exp (↑(v.asIdeal.ramificationIdx' w.asIdeal) * ↑(multiplicity v.asIdeal (Ideal.span {x}))))⁻¹ =
    (exp ↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x}))))⁻¹

Tactic:
inv_inj,

Goal state after:
case inr
A : Type u_1
B : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : Module.IsTorsionFree A B
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ exp (↑(v.asIdeal.ramificationIdx' w.asIdeal) * ↑(multiplicity v.asIdeal (Ideal.span {x}))) =
    exp ↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x})))