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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : CuspFormClass F Γ k
hk : 0 < k
hs : ↑k / 2 + 1 < s.re
⊢ HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)

Tactic:
by
  refine hasSum_Λ_of_qExpansion_isBigO hk f (r := k / 2)
    (by linarith [show (0 : ℝ) < k from mod_cast hk]) hs ?_ ?_
  · simp [Λ_eq_mellin, (CuspFormClass.zero_at_infty f).valueAtInfty_eq_zero]
  · simpa using CuspFormClass.qExpansion_isBigO f

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)

Tactic:
rw [Nat.succ_eq_add_one]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
induction n with

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)

Tactic:
refine ⟨fun H S hS ↦ H.comp ((continuous_inclusion hS).prodMap continuous_id),
    fun H ↦ ?_⟩

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ ×ˢ Set.univ.pi fun x ↦ polarCoord.source) =ᵐ[volume.prod volume] Set.univ ×ˢ Set.univ

Tactic:
← polarCoord.symm_image_target_eq_source,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ ×ˢ Set.univ.pi fun x ↦ ↑polarCoord.symm '' polarCoord.target) =ᵐ[volume.prod volume] Set.univ ×ˢ Set.univ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ (normAtPlace w) (↑(mixedEmbedding.polarCoord K).symm x) = ‖x.1 ⟨w, hw⟩‖

Tactic:
by
  simp [normAtPlace_apply_of_isReal hw]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫ (x : mixedSpace K), f x

Tactic:
← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).integral_comp
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫ (x : realMixedSpace K), f ((mixedSpaceToRealMixedSpace K).symm x) ∂volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ (∀ (a : InfinitePlace K) (b : a.IsComplex), x✝.1 a ∈ Set.Ioi 0 ∧ x✝.2 ⟨a, b⟩ ∈ Set.Ioo (-π) π) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → x✝.1 i ∈ Set.Ioi 0) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex), x✝.2 ⟨a, b⟩ ∈ Set.Ioo (-π) π

Tactic:
forall_and

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ (unitsMulComplexConjInv K).range.index ∣ 2

Tactic:
by
  suffices (powMonoidHom 2 : _ →* torsion K).range.index = 2 by
    refine this ▸ Subgroup.index_dvd_of_le ?_
    rintro _ ⟨ζ, _, rfl⟩
    exact ⟨ζ, Subtype.ext_iff.mpr (by simp [pow_two])⟩
  rw [IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right_iff_dvd]
  exact Even.two_dvd <| even_torsionOrder K

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

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

Tactic:
norm_normAtAllPlaces

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ 2 ^ rank K = |2 ^ Finset.univ.card|

Tactic:
abs_pow,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ 2 ^ rank K = |2| ^ Finset.univ.card
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inl
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.IsReal
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
have := LiesOver.extensionEmbedding_liesOver_of_isReal w hv

Goal state after:
case inl
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.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ Module.finrank v.Completion w.Completion = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult * Real.log (↑w x) - ↑(↑w).mult * (Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹) =
    ↑(↑w).mult * Real.log (↑w x) -
      ↑(↑w).mult * (Real.log (mixedEmbedding.norm ((mixedEmbedding K) x)) * (↑(finrank ℚ K))⁻¹)

Tactic:
norm_eq_norm

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

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

Tactic:
exact (hζ.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime hp hη₁ hη₂ h).dvd

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
⊢ |Real.exp (x w₀) ^ finrank ℚ K| * |(∏ w, ↑expMapBasis x ↑w)⁻¹| * |2⁻¹ ^ nrComplexPlaces K| *
      (↑(finrank ℚ K) * regulator K) =
    Real.exp (x w₀) ^ ↑(finrank ℚ K) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
abs_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |Real.exp (x w₀)| ^ finrank ℚ K * |(∏ w, ↑expMapBasis x ↑w)⁻¹| * |2⁻¹| ^ nrComplexPlaces K *
      (↑(finrank ℚ K) * regulator K) =
    Real.exp (x w₀) ^ ↑(finrank ℚ K) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K
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/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
⊢ σ (zeta n ℚ K) ^ a = (zeta n ℚ K ^ (↑((galEquivZMod n K) σ)).val) ^ a

Tactic:
galEquivZMod,

Goal state after:
n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
⊢ σ (zeta n ℚ K) ^ a = (zeta n ℚ K ^ (↑((autEquivPow K ⋯) σ)).val) ^ a
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ (span {hζ.toInteger - 1}).IsPrime

Tactic:
rw [span_singleton_prime]
  · exact hζ.zeta_sub_one_prime
  · exact Prime.ne_zero hζ.zeta_sub_one_prime

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

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

Tactic:
normAtAllPlaces_normLeOne_eq_image

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K = normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K
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
⊢ ↑(#S) < ↑(#T)

Tactic:
rw [card_T_eq A, card_S_eq]

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, (P i - N i + 1) < ↑((B + 1) ^ n)
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))

Tactic:
by
  have := (tendsto_norm_le_div_atTop₀ K).add tendsto_inv_atTop_zero
  rw [add_zero] at this
  apply this.congr'
  filter_upwards [eventually_ge_atTop 0] with s hs
  simp_rw [← Nat.le_floor_iff hs]
  rw [Ideal.card_norm_le_eq_card_norm_le_add_one, Nat.cast_add, Nat.cast_one, add_div, one_div]

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

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

Tactic:
obtain ⟨δ, hδp, hδ⟩ := Metric.continuousAt_iff.mp hf _ (norm_pos_iff.mpr hC)
    obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp
    simpa only [← dist_eq_norm_sub'] using ⟨n, (hδ (dist_comm x n ▸ hn')).le⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (fun x ↦ ‖x‖) = Valued.v.norm

Tactic:
apply UniformSpace.Completion.extension_unique (f := @norm (PadicAlgCl p) _) (g := Valued.v.norm)

Goal state after:
case hf
p : ℕ
hp : Fact (Nat.Prime p)
⊢ UniformContinuous Norm.norm

case hg
p : ℕ
hp : Fact (Nat.Prime p)
⊢ UniformContinuous Valued.v.norm

case h
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (a : PadicAlgCl p), ‖a‖ = Valued.v.norm ↑a
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]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
r : ℤ_[p]
f : C(ℤ_[p], E)
⊢ { toFun := fun x ↦ Δ_[1]^[x] (⇑(r • f)) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } =
    (RingHom.id ℤ_[p]) r • { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

Tactic:
ext n

Goal state after:
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]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
r : ℤ_[p]
f : C(ℤ_[p], E)
n : ℕ
⊢ { toFun := fun x ↦ Δ_[1]^[x] (⇑(r • f)) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } n =
    ((RingHom.id ℤ_[p]) r • { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ }) n
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
⊢ ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(V j)

Tactic:
choose r hr using hU.exists_mem

Goal state after:
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
r : X → ι
hr : ∀ (a : X), a ∈ U (r a)
⊢ ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(V j)
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case hp
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsClosed {a | ‖withValUniformEquiv a‖ ≤ 1 ↔ Valued.v a ≤ 1}

Tactic:
| hp =>

Goal state after:
Module: Mathlib.NumberTheory.Pell

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

Tactic:
induction n with

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ 0 < (a ^ n.succ).y

Tactic:
induction n with

Goal state after:
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.num ^ 2 / ↑q.den ^ 2| < ↑M / ↑q.den ^ 2

Tactic:
← div_pow,

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 - (↑q.num / ↑q.den) ^ 2| < ↑M / ↑q.den ^ 2
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

Tactic:
exact (algebraMap K L).injective.comp (FaithfulSMul.algebraMap_injective R K)

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 0 < a.x
hay : 0 ≤ a.y
⊢ ∃ n, a = a₁ ^ n

Tactic:
lift a.x to ℕ using hax.le with ax hax'
  induction ax using Nat.strong_induction_on generalizing a with | h x ih =>
  rcases hay.eq_or_lt with hy | hy
  · -- case 1: `a = 1`
    refine ⟨0, ?_⟩
    rcases eq_one_or_neg_one_iff_y_eq_zero.2 hy.symm with rfl | rfl
    · simp
    · simp at hax'
  · -- case 2: `a ≥ a₁`
    have hx₁ : 1 < a.x := by nlinarith [a.prop, h.d_pos]
    have hxx₁ := h.mul_inv_x_pos hx₁ hy
    have hxx₂ := h.mul_inv_x_lt_x hx₁ hy
    have hyy := h.mul_inv_y_nonneg hx₁ hy
    lift (a * a₁⁻¹).x to ℕ using hxx₁.le with x' hx'
    obtain ⟨n, hn⟩ := ih x' (mod_cast hxx₂.trans_eq hax'.symm) hyy hx' hxx₁
    exact ⟨n + 1, by rw [pow_succ', ← hn, mul_comm a, ← mul_assoc, mul_inv_cancel, one_mul]⟩

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: case refine_4
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 ≠ ⊥
⊢ 𝓟D.inertiaDegIn B ≤ p.inertiaDegIn B

Tactic:
rw [inertiaDegIn_eq_inertiaDeg p P Gal(L/K),
      inertiaDegIn_eq_inertiaDeg _ P (stabilizer Gal(L/K) P)]
    exact inertiaDeg_above_le 𝓟D P

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case e_f.e_s
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
n : ℕ
⊢ (s.prodPrimes.gcd n).divisors = {a ∈ s.prodPrimes.divisors | a ∣ n}

Tactic:
← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)

Goal state after:
case e_f.e_s
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
n : ℕ
⊢ {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} = {a ∈ s.prodPrimes.divisors | a ∣ n}
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ y_1, ↑((p.powQuotSuccInclusion P i) y_1) = (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)

Tactic:
refine ⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩

Goal state after:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ↑((p.powQuotSuccInclusion P i) ⟨(Quotient.mk (P ^ e)) (-z), ⋯⟩) =
    (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ q

Tactic:
refine ⟨m, hne, hlt.trans_le <| ?_⟩

Goal state after:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ C / ↑n ^ q
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_1
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑(r.num * m) / ↑(r.den • id n)

Tactic:
A

Goal state after:
case refine_1
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑m / ↑n * ↑r
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p

Tactic:
have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r := by
    rw [smul_eq_mul, id]
    nth_rewrite 4 [← Rat.num_div_den r]
    push_cast
    rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]

Goal state after:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: ⊢ volume
      (⋃ m,
        (fun x ↦ x + ↑m) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
measure_iUnion_null_iff

Goal state after:
⊢ ∀ (i : ℤ),
    volume
        ((fun x ↦ x + ↑i) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}
⊢ 0 < n

Tactic:
obtain ⟨m, hm₁, _, _⟩ := hn

Goal state after:
δ : ℕ → ℝ
x : UnitAddCircle
n m : ℕ
hm₁ : m < n
left✝ : gcd m n = 1
right✝ : ‖x - ↑(↑m / ↑n)‖ < δ n
⊢ 0 < n