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

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

Tactic:
convert! hΛ.mul_right (2 / Gammaℂ s * h Γ ^ (-s)) using 1
  · ext n
    generalize (PowerSeries.coeff n) (qExpansion (h Γ) f) = p
    rw [Gammaℂ, ← div_div, ← div_div, div_self two_ne_zero, one_div, cpow_neg (2 * _), inv_inv,
      ← ofReal_ofNat, mul_cpow_ofReal_nonneg two_pos.le Real.pi_pos.le]
    simp only [ofReal_div, ofReal_mul, ofReal_ofNat, ofReal_natCast]
    have : (2 * n / h Γ : ℂ) ^ s = 2 ^ s * n ^ s / h Γ ^ s := by
      rw [← ofReal_ofNat, ← ofReal_natCast, ← ofReal_mul,
        div_cpow_ofReal_nonneg (by grind) Γ.strictWidthInfty_nonneg, ofReal_mul,
        mul_cpow_ofReal_nonneg zero_le_two n.cast_nonneg]
    rw [this, cpow_neg, cpow_neg]
    have := Gamma_ne_zero_of_re_pos hs
    have := cpow_ne_zero_iff (y := s).mpr (.inl <| ofReal_ne_zero.mpr Γ.strictWidthInfty_pos.ne')
    field_simp
  · grind [L]

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
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (Filter.map (inclusion R A hS) (𝓝 x') ×ˢ Filter.map id (𝓝 y)) (𝓝 (f (inclusion R A hS x', y)))

Tactic:
prod_map_map_eq,

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)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (Filter.map (fun p ↦ (inclusion R A hS p.1, id p.2)) (𝓝 x' ×ˢ 𝓝 y)) (𝓝 (f (inclusion R A hS x', y)))
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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (Filter.map id (𝓝 y) ×ˢ Filter.map (inclusion R A hS) (𝓝 x')) (𝓝 (f (y, inclusion R A hS x')))

Tactic:
prod_map_map_eq,

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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (Filter.map (fun p ↦ (id p.1, inclusion R A hS p.2)) (𝓝 y ×ˢ 𝓝 x')) (𝓝 (f (y, inclusion R A hS x')))
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₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank 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)
x✝ : InfinitePlace K
⊢ x✝ ≠ w₂ ↔ f.symm x✝ ≠ f.symm w₂

Tactic:
simp [f]

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₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank 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
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    ↑|↑(Equiv.Perm.sign (g.trans e₂.symm))| *
      |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
⊢ |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|

Tactic:
Equiv.Perm.sign_abs,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank 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
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    ↑1 * |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
⊢ |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ.pi fun i ↦ (expMap_single i).source) = Set.univ

Tactic:
expMap_single,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ.pi fun i ↦ Set.univ) = Set.univ
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inr.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.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
          (ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)) (by ext; simp),
        Module.finrank_self]

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)
x✝ : InfinitePlace K
⊢ x✝ ≠ w' ↔ f.symm x✝ ≠ f.symm w'

Tactic:
simp [f]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: 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
hv : v = w.comap (algebraMap K L)
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult

Tactic:
rcases w.isUnramified_or_isRamified K with h | h

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
hv : v = w.comap (algebraMap K L)
h : IsUnramified K w
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult

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
hv : v = w.comap (algebraMap K L)
h : IsRamified K w
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult
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
⊢ regulator K / regulator ↥K⁺ = 2 ^ rank K * (↑(realUnits K ⊔ torsion K).index)⁻¹

Tactic:
← closure_realFundSystem_sup_torsion,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ regulator K / regulator ↥K⁺ = 2 ^ rank K * (↑(Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K).index)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1, if x_1 = ⟨w, hw⟩ then x ↑x_1 else 0) ∈ Set.Ico 0 1 ↔ x w ∈ Set.Ico 0 1

Tactic:
Fintype.sum_ite_eq'

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

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hj : j.Coprime n
⊢ Associated (ζ - 1) (ζ ^ j - 1)

Tactic:
refine associated_of_dvd_dvd ⟨∑ i ∈ range j, ζ ^ i, (mul_geom_sum _ _).symm⟩ ?_
  match n with
  | 0 => simp_all
  | 1 => simp_all
  | n + 2 =>
      obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hj (by lia)
      use ∑ i ∈ range m, (ζ ^ j) ^ i
      rw [mul_geom_sum, ← pow_mul, ← pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
⊢ { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C } ≃
    { I // J ∣ I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }

Tactic:
refine ((Equiv.dvd J).subtypeEquiv fun I ↦ ?_).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ J ∣ I) _)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C ↔
    IsPrincipal ↑↑((Equiv.dvd J) I) ∧ ↑(absNorm ↑↑((Equiv.dvd J) I)) ≤ s * ↑(absNorm ↑J)
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ₘ)) * Nat.card Gal(↥Fₚ/ℚ) =
    Nat.card Gal(K/ℚ)
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1

Tactic:
← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝒑 (𝓞 Fₚ) Gal(Fₚ/ℚ),

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ₚ))) =
    Nat.card Gal(K/ℚ)
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
⊢ False

Tactic:
apply hxl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
⊢ x = 0
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) < ↑((B + 1) ^ n)

Tactic:
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.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: 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 ∈ 𝓝 1, ∃ a, ∀ (b : ℕ × ℕ), a ≤ b → f b.2 / f b.1 ∈ s

Tactic:
intro s

Goal state after:
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
⊢ s ∈ 𝓝 1 → ∃ a, ∀ (b : ℕ × ℕ), a ≤ b → f b.2 / f b.1 ∈ s
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case hbc
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) ≤ A

Tactic:
· exact habs kr.1 lu.1

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ x, Valued.v x ≠ 0 ∧ Valued.v x ≠ 1

Tactic:
by
    use p
    have hp : Nat.Prime p := hp.1
    simp only [valuation_p, one_div, ne_eq, inv_eq_zero, Nat.cast_eq_zero, inv_eq_one,
      Nat.cast_eq_one]
    exact ⟨hp.ne_zero, hp.ne_one⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 < (-a⁻¹).x

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a.x < 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ (-a⁻¹).y

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
case refine_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ a.y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_3
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a ∈ {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹}

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ 0 < (-a).x

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
case refine_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.x < 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ 0 ≤ (-a).y

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
case refine_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.y ≤ 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_6
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a ∈ {-a, (-a)⁻¹, - -a, -(-a)⁻¹}

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_7
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : 0 < a.x
⊢ a ∈ {a, a⁻¹, -a, -a⁻¹}

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ 0 ≤ a⁻¹.y

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
case refine_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a.y ≤ 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_9
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a ∈ {a⁻¹, a⁻¹⁻¹, -a⁻¹, -a⁻¹⁻¹}

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < -(a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁

Tactic:
lt_neg

Goal state after:
case inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : (a₁ ^ n₂).x < -1
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁
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
n k : ℕ
⊢ 2 ^ n ≤ 2 ^ (n + k)

Tactic:
apply pow_right_mono₀

Goal state after:
case h
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
n k : ℕ
⊢ 1 ≤ 2

case a
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
n k : ℕ
⊢ n ≤ n + k
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: case h.inr
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
σvV : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation K v))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation K v))
σv : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation K v)
σK : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation K v)
γK : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) := σvV.symm (σK.symm (σv.symm (exp (m.log / ↑e))))
hγK : γK ≠ 0
x : WithVal (valuation K v)
hx : ((valuation K v) x.ofVal).log < (exp (m.log / ↑e)).log
hx₀ : x ≠ 0
⊢ ((valuation K v) x.ofVal).log * ↑(v.asIdeal.ramificationIdx' w.asIdeal) < (σw (σL (σwV ↑γL))).log

Tactic:
exact Int.mul_lt_of_lt_ediv
    (mod_cast pos_of_ne_zero (ramificationIdx'_ne_zero_of_liesOver w.asIdeal v.ne_bot)) hx

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π) + (algebraMap K[X] K⟮X⟯) (π * (q / π))) = 1

Tactic:
← mod_eq_zero

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π) + (algebraMap K[X] K⟮X⟯) (π * (q / π))) = 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
⊢ multSum d = s.nu d * s.totalMass + rem d

Tactic:
rw [rem]

Goal state after:
s : BoundingSieve
d : ℕ
⊢ multSum d = s.nu d * s.totalMass + (multSum d - s.nu d * s.totalMass)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case e_f
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
⊢ muPlus d * multSum d = s.totalMass * (muPlus d * s.nu d) + muPlus d * rem d

Tactic:
rw [rem]

Goal state after:
case e_f
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
⊢ muPlus d * multSum d = s.totalMass * (muPlus d * s.nu d) + muPlus d * (multSum d - s.nu d * s.totalMass)