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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z
⊢ 1 < (↑k).re

Tactic:
norm_cast

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z
⊢ 1 < k
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        ((-2) ^ (2 * (m + 1)) * ↑π ^ (2 * (m + 1)) * (-1) ^ (m + 1)) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))

Tactic:
norm_cast

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ (↑(Int.negSucc 0 ^ (m + 1 + 1) * ↑(2 ^ (2 * m + 1))) * π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        (↑(Int.negSucc 1 ^ (2 * (m + 1))) * π ^ (2 * (m + 1)) * ↑(Int.negSucc 0 ^ (m + 1))) /
      ↑(2 * m + 1)! =
    ↑(-(↑(2 * (2 * (m + 1))) / bernoulli (2 * (m + 1))))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
⊢ ∀ (i : ℕ), ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)

Tactic:
intro i

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
⊢ ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(∑ x ∈ range p, x))) = 0

Tactic:
norm_cast

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(∑ x ∈ range p, x))) = 0
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0

Tactic:
norm_cast

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) (↑p * b * (a ^ (p - 2) * ↑(p * (p - 1) / 2))) = 0
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: case ih
K : Type u_1
inst✝⁶ : Field K
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝³ : Algebra v.Completion w.Completion
inst✝² : IsScalarTower K v.Completion w.Completion
inst✝¹ : ContinuousSMul v.Completion w.Completion
inst✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
a✝ : WithAbs ↑v
⊢ ((extensionEmbedding w).comp (algebraMap v.Completion w.Completion)) { toCompletion := ↑a✝ } =
    (extensionEmbedding v) { toCompletion := ↑a✝ }

Tactic:
· simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply,
        ← ComplexEmbedding.LiesOver.over w.embedding v.embedding]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: m : ℤ
⊢ 8 ∣ (2 * m + 1) ^ 2 - 1

Tactic:
have eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1)) := by ring

Goal state after:
m : ℤ
eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1))
⊢ 8 ∣ (2 * m + 1) ^ 2 - 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ emultiplicity 2 (x - y) + ↑(multiplicity 2 (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)

Tactic:
norm_cast

Goal state after:
case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ emultiplicity 2 (x - y) + ↑(multiplicity 2 (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 (n + 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ ¬2 ∣ ↑k

Tactic:
norm_cast

Goal state after:
case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ ¬2 ∣ k
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 ↑2 = 1

Tactic:
norm_cast

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 2 = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
obtain hyx | hyx := le_total y x
  · iterate 3 rw [← Int.natCast_emultiplicity]
    simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.natCast_add,
      Int.natCast_pow]
    rw [← Int.natCast_dvd_natCast] at hx
    rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy
    convert! Int.two_pow_sub_pow hxy hx hn using 2
    rw [← Int.natCast_emultiplicity]
    rfl
  · simp only [Nat.sub_eq_zero_iff_le.mpr hyx,
      Nat.sub_eq_zero_iff_le.mpr (pow_le_pow_left' hyx n), emultiplicity_zero,
      top_add, add_top]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
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' (torsion K)) '' Set.range u))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0

Tactic:
QuotientGroup.coe_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
⊢ (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
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑((mixedEmbedding.polarCoord K).transHomeomorph (homeoRealMixedSpacePolarSpace K)).symm

Tactic:
OpenPartialHomeomorph.transHomeomorph_symm_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable (↑(mixedEmbedding.polarCoord K).symm ∘ ⇑(homeoRealMixedSpacePolarSpace K).symm)
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
⊢ nrRealPlaces ↥K⁺ + nrComplexPlaces ↥K⁺ = 0 + nrComplexPlaces K

Tactic:
IsTotallyReal.nrComplexPlaces_eq_zero,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ nrRealPlaces ↥K⁺ + 0 = 0 + nrComplexPlaces 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
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := ⋯
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
· 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.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
⊢ w ((complexConj K) x) = w x

Tactic:
by
  rw [← norm_embedding_eq, complexEmbedding_complexConj, Complex.norm_conj, norm_embedding_eq]

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
· rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
    exact hx.1

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
a : 𝓞 K
hx : (mixedEmbedding K) ↑a ∈ integerSet K
⊢ ζ • (mixedEmbedding K) ↑a ∈ integerSet K

Tactic:
refine mem_integerSet.mpr ⟨torsion_smul_mem_of_mem hx.1 hζ, ⟨ζ * a, by simp⟩⟩

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

Goal state before:
pp: case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ a, integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰)) x

Tactic:
obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integerSet K := by
    refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
    exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)

Goal state after:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ ∃ a, integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰)) x
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ ↑↑((unitsComplexConj K) u) = ↑↑u ↔ ∃ v, ↑((algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v) = ↑↑u

Tactic:
Units.coe_mapEquiv,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ ↑(↑(RingOfIntegers.mapRingEquiv (complexConj K).toRingEquiv) ↑u) = ↑↑u ↔ ∃ v, ↑((algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v) = ↑↑u
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : (fun a ↦ ⟨idealSetMap K J a, ⋯⟩) x✝¹ = (fun a ↦ ⟨idealSetMap K J a, ⋯⟩) x✝
⊢ x✝¹ = x✝

Tactic:
simp_rw [Subtype.ext_iff, idealSetMap_apply] at h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : ↑x✝¹ = ↑x✝
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ ¬span {↑p} ∣ under ℤ (conductor ℤ θ)

pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})

Tactic:
← Int.ideal_span_absNorm_eq_self (under ℤ (conductor ℤ θ)),

Goal state after:
K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ ¬span {↑p} ∣ span {↑(absNorm (under ℤ (conductor ℤ θ)))}

K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
classical
  rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]
  congr 2 with w i
  rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
    ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply,
    (completeBasis K).equivFunL.apply_symm_apply]
  split_ifs with hw
  · rw [hw, completeBasis_apply_of_eq]
  · simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
⊢ IsCMField K

Tactic:
have : NeZero n := ⟨by positivity⟩

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝ : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
⊢ IsCMField K
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ regOfFamily u / regOfFamily v =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
have : span ℤ (Set.range (basisOfIsMaxRank hu)) ≤ span ℤ (Set.range (basisOfIsMaxRank hv)) := by
      rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]
      exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ regOfFamily u / regOfFamily v =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this✝ : Measurable ↑expMapBasis
x : realSpace K
this : 0 ≤ (∏ w, ↑expMapBasis x ↑w)⁻¹
⊢ ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * ENNReal.ofReal (∏ w, ↑expMapBasis x ↑w)⁻¹ *
            ENNReal.ofReal (2⁻¹ ^ nrComplexPlaces K) *
          ENNReal.ofReal ↑(finrank ℚ K) *
        ENNReal.ofReal (regulator K) *
      f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      (ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
        f (↑expMapBasis x))

Tactic:
ofReal_pow (by positivity),

Goal state after:
case e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this✝ : Measurable ↑expMapBasis
x : realSpace K
this : 0 ≤ (∏ w, ↑expMapBasis x ↑w)⁻¹
⊢ ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * ENNReal.ofReal (∏ w, ↑expMapBasis x ↑w)⁻¹ *
            ENNReal.ofReal 2⁻¹ ^ nrComplexPlaces K *
          ENNReal.ofReal ↑(finrank ℚ K) *
        ENNReal.ofReal (regulator K) *
      f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      (ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
        f (↑expMapBasis x))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
h✝ : ¬x✝ = w₀
⊢ MeasurableSet (Set.Ico 0 1)

Tactic:
· exact measurableSet_Ico

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ normAtAllPlaces '' normLeOne K = ↑expMapBasis '' paramSet K

Tactic:
by
  ext x
  by_cases hx : ∀ w, 0 < x w
  · rw [← expMapBasis.right_inv (Set.mem_univ_pi.mpr hx), (injective_expMapBasis K).mem_set_image]
    simp only [normAtAllPlaces_normLeOne, Set.mem_inter_iff, Set.mem_ofPred_eq, expMapBasis_nonneg,
      Set.mem_preimage, logMap_expMapBasis, implies_true, and_true, norm_expMapBasis,
      pow_le_one_iff_of_nonneg (Real.exp_nonneg _) Module.finrank_pos.ne', Real.exp_le_one_iff,
      ne_eq, pow_eq_zero_iff', Real.exp_ne_zero, false_and, not_false_eq_true, Set.mem_univ_pi]
    refine ⟨fun ⟨h₁, h₂⟩ w ↦ ?_, fun h ↦ ⟨fun w hw ↦ by simpa [hw] using h w, by simpa using h w₀⟩⟩
    · split_ifs with hw
      · exact hw ▸ h₂
      · exact h₁ w hw
  · refine ⟨?_, ?_⟩
    · rintro ⟨a, ⟨ha, _⟩, rfl⟩
      exact (hx fun w ↦ fundamentalCone.normAtPlace_pos_of_mem ha w).elim
    · rintro ⟨a, _, rfl⟩
      exact (hx fun w ↦ expMapBasis_pos a w).elim

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

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

Tactic:
simpa using congr_arg absNorm <|
    span_singleton_eq_span_singleton.mpr <| associated_norm_zeta_sub_one p k hζ

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ∃ δ, HasDirichletDensity S δ
⊢ h.choose ≤ 1

Tactic:
exact h.choose_spec.le_one

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
c : ℕ
⊢ ↑(univ.sup fun φ ↦ ‖φ (↑c * α)‖₊) = ↑c * ↑(univ.sup fun φ ↦ ‖φ α‖₊)

Tactic:
norm_cast

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
c : ℕ
⊢ (univ.sup fun φ ↦ ‖φ (↑c * α)‖₊) = ↑c * univ.sup fun φ ↦ ‖φ α‖₊
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p m : ℕ
hpm : ¬p ∣ m
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hm : f ↑m < 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
bezout : a * ↑(p ^ k) + b * ↑(m ^ k) = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f 1 = f ↑1

Tactic:
norm_cast

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ ∃ x ∈ ↑(Finset.range (p ^ k)), dist z ↑x < ε

Tactic:
refine ⟨z.appr k, ?_, ?_⟩

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z.appr k ∈ ↑(Finset.range (p ^ k))

case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∀ c ∈ t, f c ∈ ↑V

Tactic:
intro i

Goal state after:
case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
i : α
⊢ i ∈ t → f i ∈ ↑V
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
⊢ ∀ (i : β) (j : Unit), ‖replicateCol Unit (x - y) i j‖ ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
intro i

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.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
i : β
j : Unit
⊢ ↑|x i - y i| ≤ ↑B

Tactic:
norm_cast

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
⊢ |x i - y i| ≤ ↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊
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
⊢ f ↑(ofDigits m L) = f L'.sum

Tactic:
simp [L', Nat.ofDigits_eq_sum_mapIdx]

Goal state after: