mathlib-initiative/mathlib-tactics huggingface dataset:
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))
⊢ hζ.toInteger - 1 ≠ 0

Tactic:
exact Prime.ne_zero hζ.zeta_sub_one_prime

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))
h : (span {hζ.toInteger - 1}).IsPrime
hp0 : 𝒑 ≠ ⊥
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
← Nat.totient_prime_pow_succ hp.out,

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))
h : (span {hζ.toInteger - 1}).IsPrime
hp0 : 𝒑 ≠ ⊥
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = (p ^ (k + 1)).totient
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
this✝ : IsGalois ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main : (𝒑.primesOver (𝓞 K)).ncard * (p ^ k * (p - 1)) = Nat.card Gal(K/ℚ)
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
← Nat.totient_prime_pow_succ hp.out,

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
this✝ : IsGalois ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main : (𝒑.primesOver (𝓞 K)).ncard * (p ^ (k + 1)).totient = Nat.card Gal(K/ℚ)
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1
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₂ :
  ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈
    UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
h₃ : P.inertiaDeg ℤ = (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).natDegree
⊢ P.inertiaDeg ℤ = orderOf ↑p

Tactic:
Polynomial.mem_normalizedFactors_iff
    (map_monic_ne_zero (minpoly.monic ζ.isIntegral))

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
⊢ P.inertiaDeg ℤ = orderOf ↑p
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 ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈
    UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ P.ramificationIdx ℤ = 1

Tactic:
Polynomial.mem_normalizedFactors_iff
    (map_monic_ne_zero (minpoly.monic ζ.isIntegral))

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 ∣ 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 ℤ ζ))
⊢ P.ramificationIdx ℤ = 1
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
⊢ (galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P) = Subgroup.zpowers (ZMod.unitOfCoprime p hn)

Tactic:
classical
  have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)}),
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime, inertiaDegIn_eq_of_not_dvd p K hn]

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 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ 𝒑.inertiaDegIn (𝓞 ↥Fₘ) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 ↥Fₚ) = p ^ k * (p - 1)

Tactic:
inertiaDegIn_eq_of_not_dvd p _ hm,

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 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ orderOf ↑p = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 ↥Fₚ) = p ^ k * (p - 1)
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_3
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}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
s : ℝ
⊢ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s =
    ((fun x ↦
          ↑(Nat.card
                  ↑({x_1 | x_1 ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x_1) ≤ x} ∩
                      ↑(ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) ↑↑(toMixed K)))) /
              x *
            (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)) ∘
        fun x ↦ id x * ↑(absNorm ↑J))
      s

Tactic:
Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₁ K hJ,

Goal state after:
case e'_3
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}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
s : ℝ
⊢ ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }) / s =
    ((fun x ↦
          ↑(Nat.card
                  ↑({x_1 | x_1 ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x_1) ≤ x} ∩
                      ↑(ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) ↑↑(toMixed K)))) /
              x *
            (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)) ∘
        fun x ↦ id x * ↑(absNorm ↑J))
      s
Module: Mathlib.NumberTheory.NumberField.House

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

Tactic:
use w.embedding

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
w : InfinitePlace K
hw : 1 ≤ w ↑α
⊢ 1 ≤ ‖w.embedding ↑α‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a a_1 l.1 * (newBasis K) l.2)) b) = 0 (a_1, b)
⊢ ∀ (i : α) (j : β), a i j = 0 i j

Tactic:
intro k'

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a a_1 l.1 * (newBasis K) l.2)) b) = 0 (a_1, b)
k' : α
⊢ ∀ (j : β), a k' j = 0 k' j
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ TotallyBounded Set.univ

Tactic:
by
  refine Metric.totallyBounded_iff.mpr (fun ε hε ↦ ?_)
  obtain ⟨k, hk⟩ := exists_pow_neg_lt p hε
  refine ⟨Nat.cast '' Finset.range (p ^ k), Set.toFinite _, fun z _ ↦ ?_⟩
  simp only [PadicInt, Set.mem_iUnion, Metric.mem_ball, exists_prop, Set.exists_mem_image]
  refine ⟨z.appr k, ?_, ?_⟩
  · simpa only [Finset.mem_coe, Finset.mem_range] using z.appr_lt k
  · exact (((z - z.appr k).norm_le_pow_iff_mem_span_pow k).mpr (z.appr_spec k)).trans_lt hk

Goal state after:
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
⊢ q = p

Tactic:
by_contra! hpq
    apply hq.elim.ne_one
    rw [ne_comm, ← Nat.coprime_primes hp hq.elim, hp.coprime_iff_not_dvd] at hpq
    rcases heq with ⟨_, _, heq⟩
    simpa [eq_one_of_not_dvd bdd hp0 hp1 hmin hpq] using heq q

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 ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ (logb ↑m ↑n * ↑k)

Tactic:
mul_comm (logb ..)

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 ^ (↑k * logb ↑m ↑n)
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
h : Valued.v.restrict (y - x) < ↑(Units.mk0 (Valued.v.restrict (↑p ^ n)) ⋯)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
⊢ ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ n)⁻¹

Tactic:
set y' := (WithVal.equiv (Rat.padicValuation p)) y with hy

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
h : Valued.v.restrict (y - x) < ↑(Units.mk0 (Valued.v.restrict (↑p ^ n)) ⋯)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ ↑(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
a : E
n : ℕ
x : ℤ_[p]
⊢ (mahlerTerm a n) x = (mahler n) x • a

Tactic:
by
  simp only [mahlerTerm, ContinuousMap.smul_apply', ContinuousMap.const_apply]

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

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
⊢ Valued.v.restrict (y - x) < ↑γ

Tactic:
set y' := (WithVal.equiv (Rat.padicValuation p)) y with hy

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ Valued.v.restrict (y - x) < ↑γ
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |↑d - ↑q ^ 2| < ↑M / ↑q.den ^ 2

Tactic:
←
      sq_sqrt (Int.cast_pos.mpr h₀).le,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |√↑d ^ 2 - ↑q ^ 2| < ↑M / ↑q.den ^ 2
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : (Polynomial.aeval a) (Polynomial.derivative F) + q * h = 0
⊢ (Polynomial.aeval a) (Polynomial.derivative F) = -q * h

Tactic:
by simpa using eq_neg_of_add_eq_zero_left this

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
⊢ ∃ a, IsFundamental a

Tactic:
obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ ∃ a, IsFundamental a
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) = (a.x ^ 2 - 1) * a₁.x

Tactic:
← a.prop_y

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) = d * a.y ^ 2 * a₁.x
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁹ : Field K
inst✝³⁸ : Field L
inst✝³⁷ : Algebra K L
inst✝³⁶ : CommRing A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
h𝓟 : 𝓟D ≠ ⊥
⊢ 0 < 𝓟D.ramificationIdxIn B

Tactic:
exact Nat.pos_of_ne_zero <| ramificationIdxIn_ne_zero (stabilizer Gal(L/K) P)

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

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ <
    ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
apply newton_seq_succ_dist_weak

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ (Polynomial.aeval a) F ≠ 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

Tactic:
by_cases h : d = 0

Goal state after:
case pos
s : BoundingSieve
d : ℕ
h : d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

case neg
s : BoundingSieve
d : ℕ
h : ¬d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ -1 = 0 * 0

Tactic:
by rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
⊢ ∀ p > (eval 0 f).natAbs,
    Nat.Prime p →
      ∃ n,
        ¬↑p ∣ n ∧
          ∃ gp,
            gp.natDegree ≤ p * f.natDegree - 1 ∧
              ∀ {r : ℂ},
                r ∈ f.aroots ℂ →
                  ‖↑n * cexp r - ↑p * (aeval r) gp‖ ≤
                    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then
                          (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
                        else 0) ^
                        p /
                      ↑(p - 1)!

Tactic:
intro p p_gt prime_p

Goal state after:
case h
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
⊢ ∃ n,
    ¬↑p ∣ n ∧
      ∃ gp,
        gp.natDegree ≤ p * f.natDegree - 1 ∧
          ∀ {r : ℂ},
            r ∈ f.aroots ℂ →
              ‖↑n * cexp r - ↑p * (aeval r) gp‖ ≤
                (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then
                      (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
                    else 0) ^
                    p /
                  ↑(p - 1)!
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
⊢ ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))

Tactic:
refine ⟨a, ?_, hlt⟩

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
⊢ a ∈ Finset.Icc 0 ↑b
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 < r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0

Tactic:
clear hn n

Goal state after:
r : ℝ
hr : 2 < r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬IncompRel r a b ↔ SymmGen r a b

Tactic:
rw [← not_symmGen_iff, not_not]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
⊢ Tendsto (addOrderOf ∘ u) atTop atTop

Tactic:
rw [(funext hu₀ : addOrderOf ∘ u = (↑))]

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
⊢ Tendsto Subtype.val atTop atTop