mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ((algebraMap F K).comp (algebraMap F K).rangeRestrictFieldEquiv.symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(algebraMap F K).fieldRange) K)) x✝

Tactic:
simp

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
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ↑x✝ = (algebraMap (↥(algebraMap F K).fieldRange) K) x✝
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
x✝ : ↥(maximalRealSubfield K)
⊢ ((algebraMap F K).comp (CMExtension.equivMaximalRealSubfield F K).symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(maximalRealSubfield K)) K)) x✝

Tactic:
simp

Goal state after:
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 →+* ℂ
x✝ : ℚ
⊢ (φ.comp (algebraMap ℚ K)) x✝ = (ψ.comp (algebraMap ℚ K)) x✝

Tactic:
simp

Goal state after:
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 φ σ
ν : Gal(K/ℚ)
⊢ σ = ν.symm⁻¹ * σ * ν.symm

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
A : ℤ[X]
⊢ ∀ (x : (ℤ ⧸ span {↑p})[X]),
    normalize ((mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv x) =
      (mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv (normalize x)

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
x✝ : ℤ
⊢ (((algebraMap (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})).comp
            (Int.quotientSpanNatEquivZMod p).toRingHom).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝ =
    (((RingEquiv.toRingHom ?m.136).comp (algebraMap (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}))).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ Fintype.card (ZMod p) = p ^ 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: case inl
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ hη₂ : η₁ ∈ nthRootsFinset p 1
⊢ ζ - 1 ∣ η₁ - η₁

Tactic:
simp

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
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
⊢ ↑1 = 1

Tactic:
OneMemClass.coe_one

Goal state after:
n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
⊢ 1 = 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
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 = span {hζ.toInteger - 1} ^ Module.finrank ℚ K

Tactic:
have : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K)) := by
    refine IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
          (FractionRing.algEquiv (𝓞 K) K).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))
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 = span {hζ.toInteger - 1} ^ Module.finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp (↑n * xᵢ)) = (↑n)⁻¹

Tactic:
← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ ENNReal.ofReal (∫ (x : ℝ) in Set.Iic 0, Real.exp (↑n * x)) = (↑n)⁻¹

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ 0 ≤ᵐ[volume.restrict (Set.Iic 0)] fun x ↦ Real.exp (↑n * x)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) ↑p

Tactic:
rw [← eval_one_cyclotomic_prime (R := 𝓞 K) (p := p),
    cyclotomic_eq_prod_X_sub_primitiveRoots hζ.toInteger_isPrimitiveRoot, eval_prod]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) (∏ j ∈ primitiveRoots p (𝓞 K), eval 1 (X - C j))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ {0} =ᵐ[volume] ∅

Tactic:
simp

Goal state after:
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
⊢ Fintype.card (ZMod p) = p ^ 1

Tactic:
simp

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 % orderOf ((Ideal.Quotient.mk P) hζ.toInteger) =
    p ^ i % orderOf ((Ideal.Quotient.mk P) hζ.toInteger)
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:
← h₀.eq_orderOf,

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 % n = p ^ i % n
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.RingTheory.Unramified.Dedekind

Goal state before:
pp: 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)
this : q' = Ideal.map (algebraMap B (Localization.AtPrime q)) (Ideal.map (algebraMap A B) p)
⊢ Submodule.IsPrincipal (Ideal.map (algebraMap A (Localization.AtPrime q)) p)

Tactic:
IsScalarTower.algebraMap_eq A (Localization.AtPrime p) (Localization.AtPrime q),

Goal state after:
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)
this : q' = Ideal.map (algebraMap B (Localization.AtPrime q)) (Ideal.map (algebraMap A B) p)
⊢ Submodule.IsPrincipal
    (Ideal.map
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q)).comp (algebraMap A (Localization.AtPrime p))) p)
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: 𝒪 : Type u_2
inst✝⁴ : CommRing 𝒪
inst✝³ : Module.Finite ℤ 𝒪
inst✝² : Algebra.Unramified ℤ 𝒪
inst✝¹ : IsDomain 𝒪
inst✝ : FaithfulSMul ℤ 𝒪
this✝³ : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this✝² : Algebra ℤ K := Ring.toIntAlgebra K
this✝¹ : CharZero 𝒪
this✝ : NumberField K
this : Module.finrank ℚ K = 1
⊢ ∀ (x : ℤ), (algebraMap ℤ K) x = (AlgEquiv.ofBijective (IsScalarTower.toAlgHom ℤ ℚ K) ⋯) ((algebraMap ℤ ℚ) x)

Tactic:
simp

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

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
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 𝒑
⊢ p.Coprime m

Tactic:
hp.out.coprime_iff_not_dvd

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 𝒑
⊢ ¬p ∣ m
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
x✝ : mixedSpace K
⊢ x✝ ∈ {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} ↔ x✝ ∈ normLeOne K

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', house α = ‖σ' α‖ * house α ^ (finrank ℚ K - 1)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
T : Type u_2
l : List T
y x : R
⊢ List.map (fun x_1 ↦ x • y ^ x_1.2) l.zipIdx = List.map (fun x_1 ↦ x • x_1) (List.map (fun x ↦ y ^ x.2) l.zipIdx)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (List.mapIdx (fun i x ↦ y ^ i) l).sum = (y ^ l.length - 1) / (y - 1)

Tactic:
← geom_sum_eq hy l.length,

Goal state after:
T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (List.mapIdx (fun i x ↦ y ^ i) l).sum = ∑ i ∈ Finset.range l.length, y ^ i
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : v ∈ T
⊢ A *ᵥ v ∈ S

Tactic:
mem_Icc

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inl
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
⊢ f ↑0 = AbsoluteValue.trivial ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ ∀ i_1 ∈ univ, ↑B * -(A i i_1)⁻ ≤ 0

Tactic:
intro j

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
⊢ j ∈ univ → ↑B * -(A i j)⁻ ≤ 0
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ ↑B * -(A i j)⁻ ≤ 0

Tactic:
simp only [mul_neg, Left.neg_nonpos_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ 0 ≤ ↑B * (A i j)⁻
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ ∀ i_1 ∈ univ, 0 ≤ ↑B * (A i i_1)⁺

Tactic:
intro j

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
⊢ j ∈ univ → 0 ≤ ↑B * (A i j)⁺
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ False

Tactic:
have h {n : ℕ} (hn₀ : n ≠ 0) (hn : n < a * b) : 1 ≤ f n := by
    by_contra! hn₁
    exact (not_le_of_gt hn) <| hmin n ⟨map_pos_of_ne_zero f (mod_cast hn₀), hn₁⟩

Goal state after:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
ha₀ : a ≠ 0
hb₀ : b ≠ 0
h : ∀ {n : ℕ}, n ≠ 0 → n < a * b → 1 ≤ f ↑n
⊢ False
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
i : α
x✝ : i ∈ univ
⊢ ↑n * max 1 ‖A‖ * ↑B = ∑ x, max 1 ‖A‖ * ↑B

Tactic:
simp

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
i : α
x✝ : i ∈ univ
⊢ ↑n * max 1 ‖A‖ * ↑B = ↑n * (max 1 ‖A‖ * ↑B)
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
⊢ ∏ x, (↑n * max 1 ‖A‖ * ↑B + 1) = (↑n * max 1 ‖A‖ * ↑B + 1) ^ m

Tactic:
simp

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
⊢ z ∈ ⋃ y ∈ Nat.cast '' ↑(Finset.range (p ^ k)), ball y ε

Tactic:
simp only [PadicInt, Set.mem_iUnion, Metric.mem_ball, exists_prop, Set.exists_mem_image]

Goal state after:
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 < ε
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: case zero
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M : ℕ
hMN : N ≤ M
⊢ f (M, M + 0).2 / f (M, M + 0).1 ∈ ↑t

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ ∀ (x y : ℚ), |↑(x * y)| = |↑x| * |↑y|

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ ∀ (x : ℚ), 0 ≤ |↑x|

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ ∀ (x : ℚ), |↑x| = 0 ↔ x = 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inl
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
⊢ f ↑0 ≤ 1

Tactic:
simp

Goal state after:
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₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹ = (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹

Tactic:
← mul_rpow (by positivity) (by positivity),

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₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹ = (↑n₀ * (logb ↑n₀ ↑n + 1) * ↑k) ^ (↑k)⁻¹
Module: Mathlib.NumberTheory.Ostrowski

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

Tactic:
simp

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)
⊢ f ↑n ^ k = f ↑(n ^ k)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
hfm1 : 1 < f ↑0
hm : 0 ≤ 1
⊢ f ↑0 ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
hfm1 : 1 < f ↑1
hm : 1 ≤ 1
⊢ f ↑1 ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inr.inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
⊢ f ↑1 ^ s⁻¹ = real ↑1

Tactic:
simp

Goal state after:
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)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun x ↦ r ^ x
n : ℕ
⊢ F ↑n = (r + 1) ^ n

Tactic:
rw [mahlerSeries_apply_nat hr le_rfl, (Commute.one_right _).add_pow]

Goal state after:
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)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun x ↦ r ^ x
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), n.choose i • r ^ i = ∑ m ∈ Finset.range (n + 1), r ^ m * 1 ^ (n - m) * ↑(n.choose m)
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖(algebraMap ℚ_[p] (PadicAlgCl p)) x‖ = ‖x‖

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖↑((algebraMap ℚ_[p] (PadicAlgCl p)) x)‖ = ‖x‖

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ↑‖↑((algebraMap ℚ_[p] (PadicAlgCl p)) x)‖₊ = ↑‖x‖₊

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f ↑R

Tactic:
simpa only [← Function.iterate_add_apply, add_comm, nsmul_one, add_zero] using
      (shift_eq_sum_fwdDiff_iter 1 (Δ_[1]^[n] f) R 0).symm

Goal state after: