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

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
this : (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)).index ≠ 0

Tactic:
rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
f : ℍ → ℂ
c : ℂ
⊢ (c • f) ∣[k] A = (σ A) c • f ∣[k] A

Tactic:
ext τ : 1
  simp only [slash_apply, Pi.smul_apply, smul_eq_mul, map_mul, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • (mapGL ℝ).range).Commensurable (mapGL ℝ).range

Tactic:
rw [MonoidHom.range_eq_map]

Goal state after:
g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤).Commensurable
    (Subgroup.map (mapGL ℝ) ⊤)
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: case mpr
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ (∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsBoundedAtImInfty (f ∣[k] γ)) → c.IsBoundedAt f k

Tactic:
rintro ⟨γ, rfl, b⟩

Goal state after:
case mpr
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
b : IsBoundedAtImInfty (f ∣[k] γ)
hc : IsCusp ((mapGL ℝ) γ • ∞) (mapGL ℝ).range
⊢ ((mapGL ℝ) γ • ∞).IsBoundedAt f k
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: case mpr
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ (∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsZeroAtImInfty (f ∣[k] γ)) → c.IsZeroAt f k

Tactic:
rintro ⟨γ, rfl, b⟩

Goal state after:
case mpr
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
b : IsZeroAtImInfty (f ∣[k] γ)
hc : IsCusp ((mapGL ℝ) γ • ∞) (mapGL ℝ).range
⊢ ((mapGL ℝ) γ • ∞).IsZeroAt f k
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : -upperRightHom x ∈ 𝒢
hgi : ↑(-upperRightHom x) 1 0 = 0
⊢ upperRightHom (2 • x) ∈ 𝒢

Tactic:
simpa only [AddChar.map_nsmul_eq_pow, neg_sq] using pow_mem hgg 2

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsZeroAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
simp_rw [IsZeroAtImInfty, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe,
        FunLike.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto ((σ g) (c • 1) • ⇑f ∣[k] g) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : (↑g).det = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1

Tactic:
rw [det_fin_two, hc] at had

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 0 = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

pp: case inr
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
· use g 0 1
    suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]
    ext i j; fin_cases i <;> fin_cases j <;>
      simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Goal state after:
case inr
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : normSq ↑z < 1
imz : 0 < z.im
⊢ z.im < z.im / normSq ↑z

Tactic:
apply (lt_div_iff₀ z.normSq_pos).mpr

Goal state after:
z : ℍ
h : normSq ↑z < 1
imz : 0 < z.im
⊢ z.im * normSq ↑z < z.im
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case e_f
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ (2 * ↑π * Complex.I)⁻¹ * ↑(2 * π / h) * (𝕢 h ↑τ * Complex.I) • (cuspFunction h f (𝕢 h ↑τ) / 𝕢 h ↑τ ^ (n + 1)) =
    1 / ↑h * (1 / 𝕢 h ↑τ ^ n * f { coe := ↑τ, coe_im_pos := ⋯ })

Tactic:
show ⟨↑τ, τ.2⟩ = τ by rfl,

Goal state after:
case e_f
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ (2 * ↑π * Complex.I)⁻¹ * ↑(2 * π / h) * (𝕢 h ↑τ * Complex.I) • (cuspFunction h f (𝕢 h ↑τ) / 𝕢 h ↑τ ^ (n + 1)) =
    1 / ↑h * (1 / 𝕢 h ↑τ ^ n * f τ)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ (fun τ ↦ f τ - valueAtInfty f) =O[atImInfty] fun τ ↦ rexp (-2 * π * τ.im / h)

Tactic:
have := hfbdd.comp_tendsto tendsto_comap_im_ofComplex

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
⊢ (fun τ ↦ f τ - valueAtInfty f) =O[atImInfty] fun τ ↦ rexp (-2 * π * τ.im / h)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : ModularForm Γ a
g : ModularForm Γ b
⊢ qExpansion h ⇑(((DirectSum.of (ModularForm Γ) a) f * (DirectSum.of (ModularForm Γ) b) g) (a + b)) =
    qExpansion h ⇑f * qExpansion h ⇑g

Tactic:
by
  simpa [DirectSum.of_mul_of] using! ModularForm.qExpansion_mul hh hΓ f g

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
m : ℕ
⊢ c m = (PowerSeries.coeff m) (qExpansion h ⇑f)

Tactic:
by
  have h1 := (hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf).hasFPowerSeriesAt
  have h2 := (hasFPowerSeries_cuspFunction f hh hfanalytic hf).hasFPowerSeriesAt
  simpa using congr_arg (FormalMultilinearSeries.coeff · m) (h1.eq_formalMultilinearSeries h2)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ (symmetricIco G).filter ≤ atTop

Tactic:
symmetricIco,

Goal state after:
G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ { filter := Filter.map (fun N ↦ Ico (-N) N) atTop }.filter ≤ atTop
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: hmem : 0 ∈ Metric.ball 0 1
⊢ (PowerSeries.coeff 1) (qExpansion 1 Δ) = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0

Tactic:
by
        simp [qExpansion_coeff, ← derivWithin_of_isOpen Metric.isOpen_ball hmem]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
m : ℤ
this : Summable fun n ↦ ((↑m * ↑z + ↑n + 1) * (↑m * ↑z + ↑n))⁻¹
⊢ Summable fun b ↦ 1 / (↑m * ↑z + ↑b) - 1 / (↑m * ↑z + ↑b + 1)

Tactic:
rw [← Finset.summable_compl_iff (s := {0, -1})] at *

Goal state after:
z : ℍ
m : ℤ
this : Summable fun x ↦ ((↑m * ↑z + ↑↑x + 1) * (↑m * ↑z + ↑↑x))⁻¹
⊢ Summable fun x ↦ 1 / (↑m * ↑z + ↑↑x) - 1 / (↑m * ↑z + ↑↑x + 1)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this✝ : ModularFormClass
  (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
    (0 *
      ↑(Nat.card
          (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
  (Matrix.SpecialLinearGroup.mapGL ℝ).range 0 :=
  Eq.mpr
    (id
      (congrArg
        (fun _a ↦
          ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range _a)
            (Matrix.SpecialLinearGroup.mapGL ℝ).range 0)
        (zero_mul
          ↑(Nat.card
              (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range)))))
    inferInstance
this : (ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range (f - const (f I))) I = 0
hc : f = const (f I)
⊢ Function.const ℍ (f I) = Function.const ℍ (Function.const ℍ (f I) I)

Tactic:
Function.const_apply

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this✝ : ModularFormClass
  (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
    (0 *
      ↑(Nat.card
          (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
  (Matrix.SpecialLinearGroup.mapGL ℝ).range 0 :=
  Eq.mpr
    (id
      (congrArg
        (fun _a ↦
          ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range _a)
            (Matrix.SpecialLinearGroup.mapGL ℝ).range 0)
        (zero_mul
          ↑(Nat.card
              (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range)))))
    inferInstance
this : (ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range (f - const (f I))) I = 0
hc : f = const (f I)
⊢ Function.const ℍ (f I) = Function.const ℍ (f I)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: w✝ : ℤ
⊢ (1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1

Tactic:
rw [add_assoc, ← add_mul, Int.add_mul_emod_self_right]

Goal state after:
w✝ : ℤ
⊢ 1 % 4 = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Continuous (measurableEquivRealMixedSpacePolarSpace K).invFun

Tactic:
by
    change Continuous fun x : polarSpace K ↦
      (⟨fun w ↦ x.1 w.val, fun w ↦ ⟨x.1 w.val, x.2 w⟩⟩ : realMixedSpace K)
    fun_prop

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✝ : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
x : K
⊢ φ ((complexConj K) x) = (starRingEnd ℂ) (φ x)

Tactic:
rw [IsConj.eq (isConj_complexConj K φ), RCLike.star_def]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ ↑|(Algebra.norm ℚ) ↑↑(preimageOfMemIntegerSet a)| = mixedEmbedding.norm ↑a

Tactic:
← norm_eq_norm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ mixedEmbedding.norm ((mixedEmbedding K) ↑↑(preimageOfMemIntegerSet a)) = mixedEmbedding.norm ↑a
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ), Polynomial.map (Int.castRingHom (ZMod p)) Q}

Tactic:
span_pair_comm,

Goal state after:
K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) Q, Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
⊢ (φ ^ orderOf φ) (root P) = root P

Tactic:
simp [pow_orderOf_eq_one φ]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx : x ∈ torsion K
⊢ ∀ ⦃a₂ : ↥(torsion K)⦄, I.torsionMapQuot ⟨x, hx⟩ = I.torsionMapQuot a₂ → ⟨x, hx⟩ = a₂

Tactic:
⟨y, hy⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx : x ∈ torsion K
y : (𝓞 K)ˣ
hy : y ∈ torsion K
⊢ I.torsionMapQuot ⟨x, hx⟩ = I.torsionMapQuot ⟨y, hy⟩ → ⟨x, hx⟩ = ⟨y, hy⟩
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
⊢ (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)

Tactic:
let τ := IsFractionRing.stabilizerHom Gal(K/ℚ) (Ideal.span {(p : ℤ)}) P
     (ℤ ⧸ span {(p : ℤ)}) (𝓞 K ⧸ P) ⟨σ, hσ⟩

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σ⟩
⊢ (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)
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)) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))

Tactic:
← Nat.totient_prime hp.out,

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.totient) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
⊢ N i ≤ (fun i ↦ ∑ j, A i j * v j) i

Tactic:
simp only [mul_neg]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
⊢ ∑ x, -(↑B * (A i x)⁻) ≤ ∑ j, A i j * v j
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
⊢ (fun i ↦ ∑ j, A i j * v j) i ≤ P i

Tactic:
simp only [mul_neg]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
⊢ ∑ j, A i j * v j ≤ ∑ j, ↑B * (A i j)⁺
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ ↑k < x ^ logb M (1 / 2)

Tactic:
by
      apply rpow_lt_rpow_of_exponent_gt hx0 hx1
      rw [hk]
      push_cast
      exact lt_add_of_le_of_pos (Nat.le_ceil _) zero_lt_one

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: case succ
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
k : ℕ
ih : f (M, M + k).2 / f (M, M + k).1 ∈ ↑t
⊢ f (M, M + (k + 1)).2 / f (M, M + (k + 1)).1 ∈ ↑t

Tactic:
simpa using! t.mul_mem (hN _ (by lia : N ≤ M + k)) ih

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
⊢ ∀ (x y z : C(X, Y)), dist x z ≤ max (dist x y) (dist y z)

Tactic:
intro f

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f : C(X, Y)
⊢ ∀ (y z : C(X, Y)), dist f z ≤ max (dist f y) (dist y z)
Module: Mathlib.Topology.Algebra.Monoid.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝⁴ : TopologicalSpace A
inst✝³ : AddMonoidWithOne A
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
hdr : DenseRange Nat.cast
κ₁ κ₂ : AddChar A M
hκ₁ : Continuous ⇑κ₁
hκ₂ : Continuous ⇑κ₂
h : κ₁ 1 = κ₂ 1
⊢ κ₁ = κ₂

Tactic:
refine DFunLike.coe_injective <| hdr.equalizer hκ₁ hκ₂ (funext fun n ↦ ?_)
  simp only [Function.comp_apply, ← nsmul_one, h, AddChar.map_nsmul_eq_pow]

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

Goal state before:
pp: case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ∑ r, house ((algebraMap (𝓞 K) K) ↑(x (l, r)) * (algebraMap (𝓞 K) K) ((newBasis K) r)) ≤
    ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r))

Tactic:
gcongr with r _; convert! house_mul_le ..
    simp only [map_intCast, house_intCast, Int.cast_abs, Int.norm_eq_abs]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
⊢ f.IsEquiv real

Tactic:
rw [← exists_nat_rpow_iff_isEquiv]

Goal state after:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = real ↑n
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: 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)
⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = real ↑n

Tactic:
have hs0 : 0 < s := hs ▸ logb_pos (mod_cast oneltm) hfm1

Goal state after:
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
⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = real ↑n
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ‖↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial‖ ≤ 1

Tactic:
rw [norm_div, div_le_one (by simpa using k.factorial_ne_zero)]
    exact x.norm_ascPochhammer_le k

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
t : ℕ
ht : ↑p ^ (-↑t) < δ
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
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
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k ↦ k.choose j • a j) 0 =
    ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k ↦ ↑(k.choose j)) 0 • a j

Tactic:
by
    simp only [fwdDiff_iter_eq_sum_shift, zero_add, sum_smul, smul_assoc,
      natCast_zsmul]

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
⊢ DenseRange ⇑tensorHom

Tactic:
intro f

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
⊢ f ∈ closure (Set.range ⇑tensorHom)