mathlib-initiative/mathlib-tactics huggingface dataset:
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
φ : K →+* ℂ
x : K
⊢ star (φ x) = (starRingEnd ℂ) (φ x)

Tactic:
RCLike.star_def

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
x : K
⊢ (starRingEnd ℂ) (φ x) = (starRingEnd ℂ) (φ x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ mixedSpaceOfRealSpace (normAtAllPlaces a) ∈ A

Tactic:
← hA,

Goal state after:
case refine_1.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ mixedSpaceOfRealSpace (normAtAllPlaces a) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

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

Tactic:
obtain hw | hw := isReal_or_isComplex w

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

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.PolarCoord

Goal state before:
pp: case refine_1
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
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ x ∈ A

Tactic:
← hA,

Goal state after:
case refine_1
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
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A
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 ∣ Nat.card ↥(torsion K)

Tactic:
exact even_iff_two_dvd.mp (even_torsionOrder K)

Goal state after:
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 : ℝ
n : ℕ
x✝ : ↑(integerSet K)
⊢ mixedEmbedding.norm ↑x✝ = ↑n ↔ absNorm ↑↑((integerSetEquiv K) x✝).1 = n

Tactic:
simp_rw [← intNorm_coe, intNorm,
        Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
h_eq : 2 * (unitsMulComplexConjInv K).range.index = 2
h : indexRealUnits K = 2
⊢ (unitsMulComplexConjInv K).range.index = 1

Tactic:
Nat.mul_eq_left two_ne_zero

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
h_eq : (unitsMulComplexConjInv K).range.index = 1
h : indexRealUnits K = 2
⊢ (unitsMulComplexConjInv K).range.index = 1
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
x✝ : w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
cases LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq w v with

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

Goal state before:
pp: case refine_2
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
this : L = ⊤
⊢ E ⊔ maximalRealSubfield K = ⊤

Tactic:
simpa [L] using congr_arg IntermediateField.toSubfield this

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

Goal state before:
pp: case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
⊢ ¬L = ⊥

Tactic:
contrapose h

Goal state after:
case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : L = ⊥
⊢ maximalRealSubfield K ≤ E
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |∑ x,
          of (fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            (f (f.symm w')) (f (f.symm x))| *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|

Tactic:
Equiv.apply_symm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |∑ x,
          of (fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            w' x| *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ ↑expMap ((completeBasis K) ↑i) =
    normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))))

Tactic:
rw [completeBasis_apply_of_ne, expMap.right_inv (by simp [expMap_target, pos_at_place])]

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)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ f.symm w' →
      ∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            i j =
        0

Tactic:
simp_rw [Equiv.forall_congr_left f, ← f.symm.sum_comp, reindex_apply, submatrix_apply,
      of_apply, f.symm_symm, f.apply_symm_apply, Finset.sum_dite_irrel, ne_eq,
      EmbeddingLike.apply_eq_iff_eq]
    intro _ h
    rw [dif_neg h, sum_mult_mul_log]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1,
      Real.exp (x w₀) ^ x_1.mult *
        (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
prod_mul_distrib,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ x_1, Real.exp (x w₀) ^ x_1.mult) *
      ∏ x_1, (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
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))
⊢ (algebraMap ℤ (𝓞 K)) ↑p ∈ span {hζ.toInteger - 1}

Tactic:
algebraMap_int_eq,

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))
⊢ (Int.castRingHom (𝓞 K)) ↑p ∈ span {hζ.toInteger - 1}
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))
σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K
| span {σ (hζ.toInteger - 1)}

Tactic:
rw [span_singleton_eq_span_singleton.mpr
      (hζ.toInteger_isPrimitiveRoot.associated_sub_one_map_sub_one σ).symm]

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))
σ : 𝓞 K ≃ₐ[ℤ] 𝓞 K
| span {hζ.toInteger - 1}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
C : ℝ
hC : ∀ x ∈ ↑expMapBasis '' paramSet K, ‖x‖ ≤ C
x : mixedSpace K
hx : x ∈ normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K
⊢ ‖x‖ ≤ C

Tactic:
rw [norm_eq_sup'_normAtPlace]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
C : ℝ
hC : ∀ x ∈ ↑expMapBasis '' paramSet K, ‖x‖ ≤ C
x : mixedSpace K
hx : x ∈ normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K
⊢ (univ.sup' ⋯ fun w ↦ (normAtPlace w) x) ≤ C
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case refine_2
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 := ⋯.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.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ ↑1 ≤
    emultiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))

Tactic:
ENat.natCast_one

Goal state after:
case refine_2
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 := ⋯.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.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ 1 ≤
    emultiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
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
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main :
  (𝒑.primesOver (𝓞 ↥Fₘ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₘ) * 𝒑.inertiaDegIn (𝓞 ↥Fₘ)) *
      ((𝒑.primesOver (𝓞 ↥Fₚ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₚ) * 𝒑.inertiaDegIn (𝓞 ↥Fₚ))) =
    (𝒑.primesOver (𝓞 K)).ncard * (𝒑.ramificationIdxIn (𝓞 K) * 𝒑.inertiaDegIn (𝓞 K))
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1

Tactic:
← ncard_primesOver_mul_ncard_primesOver Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ),

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main :
  (𝒑.primesOver (𝓞 ↥Fₘ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₘ) * 𝒑.inertiaDegIn (𝓞 ↥Fₘ)) *
      ((𝒑.primesOver (𝓞 ↥Fₚ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₚ) * 𝒑.inertiaDegIn (𝓞 ↥Fₚ))) =
    (𝒑.primesOver (𝓞 ↥Fₘ)).ncard * (Pₘ.primesOver (𝓞 K)).ncard * (𝒑.ramificationIdxIn (𝓞 K) * 𝒑.inertiaDegIn (𝓞 K))
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
⊢ (fun x ↦ f x ^ c) = ⇑g

Tactic:
ext1 x

Goal state after:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f x ^ c = g x
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ ↑(#(Icc (∑ j, ↑B * -(A i j)⁻) (∑ j, ↑B * (A i j)⁺))) = P i - N i + 1

Tactic:
rw [Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)]

Goal state after:
case e_f
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ P i + 1 - N i = P i - N i + 1
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑B + 1) ^ (↑n - ↑m) * (↑B + 1) ^ m = (↑B + 1) ^ n

Tactic:
← rpow_natCast,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑B + 1) ^ (↑n - ↑m) * (↑B + 1) ^ ↑m = (↑B + 1) ^ n
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑B + 1) ^ (↑n - ↑m + ↑m) = (↑B + 1) ^ n

Tactic:
← rpow_natCast,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑B + 1) ^ (↑n - ↑m + ↑m) = (↑B + 1) ^ ↑n
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hpq : p.Coprime q
⊢ q = 1

Tactic:
hp.coprime_iff_not_dvd

Goal state after:
case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hpq : ¬p ∣ q
⊢ q = 1
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:
← rpow_natCast,

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:

Tactic:
f n = (f ↑(n ^ k)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, map_pow, ← rpow_natCast, rpow_rpow_inv (by positivity) (by positivity)]
    _ ≤ (n₀ * (logb n₀ ↑(n ^ k) + 1)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact h_ineq1 <| one_le_pow₀ (one_le_iff_ne_zero.mpr h₀)
    _ = (n₀ * (k * logb n₀ n + 1)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, logb_pow]
    _ ≤ (n₀ * (k * logb n₀ n + k)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact one_le_cast.mpr hk
    _ = (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ := by
      rw [← mul_rpow (by positivity) (by positivity), mul_assoc, add_mul, one_mul,
        mul_comm _ (k : ℝ)]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

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

Tactic:
by
  contrapose! notbdd with h
  intro n
  have h_ineq1 {m : ℕ} (hm : 1 ≤ m) : f m ≤ n₀ * (logb n₀ m + 1) := by
    /- L is the string of digits of `n` in the base `n₀` -/
    set L := Nat.digits n₀ m
    calc
    f m ≤ (L.mapIdx fun i _ ↦ n₀ * f n₀ ^ i).sum := apply_le_sum_digits m hn₀
    _ ≤ (L.mapIdx fun _ _ ↦ (n₀ : ℝ)).sum := by
      simp only [List.mapIdx_eq_zipIdx_map]
      refine List.sum_le_sum fun ⟨i, a⟩ _ ↦ ?_
      exact mul_le_of_le_one_right (by positivity) (pow_le_one₀ (by positivity) h)
    _ = n₀ * (Nat.log n₀ m + 1) := by
      rw [List.mapIdx_eq_zipIdx_map, List.eq_replicate_of_mem (a := (n₀ : ℝ)) (l := L.zipIdx.map _),
        List.sum_replicate, List.length_map, List.length_zipIdx, nsmul_eq_mul, mul_comm,
        Nat.length_digits n₀ m hn₀ (ne_zero_of_lt hm), Nat.cast_add_one]
      simp +contextual
    _ ≤ n₀ * (logb n₀ m + 1) := by
      gcongr
      exact natLog_le_logb ..
  -- For h_ineq2 we need to exclude the case n = 0.
  rcases eq_or_ne n 0 with rfl | h₀
  · simp
  have h_ineq2 (k : ℕ) (hk : 0 < k) :
      f n ≤ (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ := by
    have : 0 ≤ logb n₀ n := logb_nonneg (mod_cast hn₀) (mod_cast one_le_iff_ne_zero.mpr h₀)
    calc
    f n = (f ↑(n ^ k)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, map_pow, ← rpow_natCast, rpow_rpow_inv (by positivity) (by positivity)]
    _ ≤ (n₀ * (logb n₀ ↑(n ^ k) + 1)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact h_ineq1 <| one_le_pow₀ (one_le_iff_ne_zero.mpr h₀)
    _ = (n₀ * (k * logb n₀ n + 1)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, logb_pow]
    _ ≤ (n₀ * (k * logb n₀ n + k)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact one_le_cast.mpr hk
    _ = (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ := by
      rw [← mul_rpow (by positivity) (by positivity), mul_assoc, add_mul, one_mul,
        mul_comm _ (k : ℝ)]
-- For 0 < logb n₀ n below we also need to exclude n = 1.
  rcases eq_or_ne n 1 with rfl | h₁
  · simp
  refine le_of_tendsto_of_tendsto tendsto_const_nhds ?_ (eventually_atTop.mpr ⟨1, h_ineq2⟩)
  have : 0 < logb n₀ n := logb_pos (mod_cast hn₀) (by norm_cast; lia)
  simpa using (tendsto_const_rpow_inv (by positivity)).mul tendsto_nat_rpow_inv

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case hbc
f : AbsoluteValue ℚ ℝ
m✝ n✝ : ℕ
hm✝ : 1 < m✝
hn✝ : 1 < n✝
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := ⋯
hfm : 1 < f ↑m
⊢ f ↑m ^ d ≤ f ↑m ^ logb ↑m ↑n

Tactic:
← rpow_natCast,

Goal state after:
case hbc
f : AbsoluteValue ℚ ℝ
m✝ n✝ : ℕ
hm✝ : 1 < m✝
hn✝ : 1 < n✝
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
hfm : 1 < f ↑m
⊢ f ↑m ^ ↑d ≤ f ↑m ^ logb ↑m ↑n
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ (mahlerSeries fun x ↦ r ^ x) 0 = 1

Tactic:
rw [← Nat.cast_zero, mahlerSeries_apply_nat hr le_rfl, zero_add, Finset.sum_range_one,
      Nat.choose_self, pow_zero, one_smul]

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

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

Tactic:
ext; simp [mahlerTerm_apply]

Goal state after: