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

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst✝³ : ModularFormClass F Γ k
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : DiscreteTopology ↥Γ
inst✝ : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
⊢ (fun τ ↦ f τ - valueAtInfty ⇑f) =O[atImInfty] fun τ ↦ rexp (-(2 * π / Γ.strictWidthInfty) * τ.im)

Tactic:
convert! exp_decay_sub_atImInfty hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f) using
    3 with τ

Goal state after:
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst✝³ : ModularFormClass F Γ k
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : DiscreteTopology ↥Γ
inst✝ : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
τ : ℍ
⊢ -(2 * π / Γ.strictWidthInfty) * τ.im = -2 * π * τ.im / Γ.strictWidthInfty
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
by
  conv => enter [1, C, τ, 1]; rw [← norm_norm]
  refine ModularGroup.exists_bound_of_subgroup_invariant (by fun_prop) (fun g ↦ ?_)
    fun g hg τ ↦ SlashInvariantFormClass.norm_petersson_smul hg
  apply IsZeroAtImInfty.isBoundedAtImInfty
  rw [IsZeroAtImInfty, ZeroAtFilter, ← tendsto_zero_iff_norm_tendsto_zero]
  simp_rw [← UpperHalfPlane.petersson_slash_SL]
  have : ((toConjAct (g : GL (Fin 2) ℝ)⁻¹) • Γ).IsArithmetic := by
    simpa [(show Rat.castHom ℝ = algebraMap ℚ ℝ by rfl), map_inv, map_mapGL]
      using! Subgroup.IsArithmetic.conj Γ (mapGL ℚ g)⁻¹
  exact (zero_at_infty <| CuspForm.translate f g).petersson_isZeroAtImInfty_left k _
    (ModularForm.translate f' g)

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
⊢ IsZeroAtImInfty ⇑f

Tactic:
have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
  have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
  have hanal := ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ
  have hper := periodic_comp_ofComplex f hΓ
  simp_rw [IsZeroAtImInfty, ZeroAtFilter, ← h, ← cuspFunction_apply_zero hh hanal hper]
  exact (hanal.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)).congr
    (fun τ ↦ SlashInvariantFormClass.eq_cuspFunction f τ hΓ hh.ne')

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

Goal state before:

Tactic:
(qExpansion 1 Δ).coeff 1
      = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0 := by
        simp [qExpansion_coeff, ← derivWithin_of_isOpen Metric.isOpen_ball hmem]
    _ = derivWithin (fun q ↦ q * ∏' i, (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1) 0 :=
        derivWithin_congr discriminant_cuspFunction_eqOn (discriminant_cuspFunction_eqOn hmem)
    _ = 1 := by
        simp [derivWithin_fun_mul differentiableWithinAt_fun_id
          (differentiableOn_tprod_one_sub_pow_pow 24 _ hmem),
          derivWithin_id' _ _ (Metric.isOpen_ball.uniqueDiffWithinAt hmem)]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
c : ℂ
a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [mul_div_assoc]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
⊢ qExpansion 1 ⇑f = 0

Tactic:
obtain ⟨c4, hc4⟩ : ∃ c4, c4 • E₄ = f.mul f :=
    (finrank_eq_one_iff_of_nonzero' E₄ (E_ne_zero _ ⟨2, rfl⟩)).mp
      (Module.rank_eq_one_iff_finrank_eq_one.mp levelOne_weight_four_rank_one) _

Goal state after:
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
⊢ qExpansion 1 ⇑f = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d)) =
    2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m))

Tactic:
← Summable.tsum_mul_left

Goal state after:
z : ℍ
d : ℕ+
⊢ ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d)) =
    ∑' (i : ℕ+), 2 / ↑z * (1 / (-↑↑d / ↑z - ↑↑i) + 1 / (-↑↑d / ↑z + ↑↑i))

case hf
z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < ‖↑x‖ ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im
⊢ 1 < ‖↑{ coe := ↑x + ↑↑a * Complex.I, coe_im_pos := ⋯ }‖

Tactic:
rw [← one_lt_normSq_iff]
      convert! this
      simp [← normSq_eq_norm_sq, normSq_apply]
      ring

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hx : ∀ (i : ι), IsUnit (x i)
hxr : ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
⊢ ∃ b, x * b = 1 ∧ b * x = 1

Tactic:
use .mk (fun i ↦ (hx i).unit.inv) (by
    filter_upwards [hxr] with i ⟨h, hu⟩
    have hu : (hx i).unit.1 * hu.unit.inv = 1 := Subtype.val_inj.2 hu.mul_val_inv
    simp [← Units.eq_inv_of_mul_eq_one_left hu])

Goal state after:
case h
ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hx : ∀ (i : ι), IsUnit (x i)
hxr : ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
⊢ x * mk (fun i ↦ ⋯.unit.inv) ⋯ = 1 ∧ mk (fun i ↦ ⋯.unit.inv) ⋯ * x = 1
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))
⊢ ∀ (x : Y × Πʳ (i : ι), [R i, A i]), Tendsto f (𝓝 x) (𝓝 (f x))

Tactic:
rintro ⟨y, x⟩

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]
⊢ Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(mixedEmbedding.polarCoord K).symm

Tactic:
rw [polarCoord_symm_eq]
  exact (Homeomorph.measurable _).comp (measurable_polarCoordReal_symm K)

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

Goal state before:
pp: case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
· rw [Set.mem_ofPred_eq, unitSMul_smul, map_mul, norm_unit, one_mul]
    exact hx.2

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

Goal state before:
pp: case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) (↑x * ↑u * ↑↑(unitsNonZeroDivisorsEquiv.symm u⁻¹))) = (mixedEmbedding K) ↑↑x

Tactic:
map_inv,

Goal state after:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) (↑x * ↑u * ↑↑(unitsNonZeroDivisorsEquiv.symm u)⁻¹)) = (mixedEmbedding K) ↑↑x
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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ (starRingEnd ℂ) ↑((Units.complexEmbedding φ) ↑ζ) = φ ((algebraMap (𝓞 K) K) ↑↑ζ)⁻¹

Tactic:
Complex.conj_rootsOfUnity (n := torsionOrder K),

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ ↑((Units.complexEmbedding φ) ↑ζ)⁻¹ = φ ((algebraMap (𝓞 K) K) ↑↑ζ)⁻¹

K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ (Units.complexEmbedding φ) ↑ζ ∈ rootsOfUnity (torsionOrder K) ℂ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ (IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n) ∧ ↑J ∣ ↑x✝ ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n

Tactic:
and_comm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
⊢ (completeBasis K).equivFunL (↑↑(completeBasis K).equivFunL.symm ((completeBasis K) w)) i =
    if h : w = w₀ then ↑i.mult
    else ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, h⟩))))

Tactic:
ContinuousLinearMap.coe_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
⊢ (completeBasis K).equivFunL (↑(completeBasis K).equivFunL.symm ((completeBasis K) w)) i =
    if h : w = w₀ then ↑i.mult
    else ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, h⟩))))
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

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

Tactic:
span_union,

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ span ↑(Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p})) ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q}
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regulator K =
    |(Matrix.of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

Tactic:
by
  rw [regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) ∈
    normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))

Tactic:
← mem_primesOver_iff_mem_normalizedFactors _ (by simp [NeZero.ne p])

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) ∈
    (span {↑p}).primesOver (𝓞 K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |(∏ x_1, ↑(smulRight 1 (deriv_expMap_single x_1 ((completeBasis K).equivFun.symm x x_1))) 1) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
ContinuousLinearMap.coe_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |(∏ x_1, (smulRight 1 (deriv_expMap_single x_1 ((completeBasis K).equivFun.symm x x_1))) 1) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet (paramSet K)

Tactic:
by
  refine MeasurableSet.univ_pi fun _ ↦ ?_
  split_ifs
  · exact measurableSet_Iic
  · exact measurableSet_Ico

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

Tactic:
by
  have h := isPrime_span_zeta_sub_one p k hζ
  have hp0 : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero
  rw [← Nat.totient_prime_pow_succ hp.out, ← finrank _ K,
    IsDedekindDomain.ramificationIdx_eq_multiplicity 𝒑, map_eq_span_zeta_sub_one_pow p k hζ,
    multiplicity_pow_self (span_zeta_sub_one_ne_bot p k hζ) (isUnit_iff.not.mpr h.ne_top)]
  exact map_ne_bot_of_ne_bot hp0

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsBounded (normLeOne K)

Tactic:
by
  classical
  rw [normLeOne_eq_preimage]
  suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
  refine IsBounded.subset ?_ (Set.image_mono subset_closure)
  exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)

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

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left✝ : P.IsPrime
right✝ : P.LiesOver 𝒑
⊢ 𝒑.ramificationIdxIn (𝓞 K) = 1

Tactic:
ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ),

Goal state after:
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left✝ : P.IsPrime
right✝ : P.LiesOver 𝒑
⊢ P.ramificationIdx ℤ = 1
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 : ↥(Ideal (𝓞 K))⁰
⊢ ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C ↔
    ClassGroup.mk0 ⟨↑↑((Equiv.dvd J) I), ⋯⟩ = 1 ∧ ↑(absNorm ↑↑((Equiv.dvd J) I)) ≤ s * ↑(absNorm ↑J)

Tactic:
simp_rw [Equiv.dvd_apply, Submonoid.coe_mul, ← Submonoid.mul_def, _root_.map_mul, hJ,
    inv_mul_eq_one, Nat.cast_mul, mul_comm s, eq_comm, and_comm, and_congr_left_iff]

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))⁰
⊢ C = ClassGroup.mk0 I → (↑(absNorm ↑I) ≤ s ↔ ↑(absNorm ↑J) * ↑(absNorm ↑I) ≤ ↑(absNorm ↑J) * s)
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⁻¹
⊢ Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C } =
    Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }

Tactic:
by
  simp_rw [← nonZeroDivisors_dvd_iff_dvd_coe]
  refine Nat.card_congr ?_
  refine ((Equiv.dvd J).subtypeEquiv fun I ↦ ?_).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ J ∣ I) _)
  rw [← ClassGroup.mk0_eq_one_iff (SetLike.coe_mem _)]
  simp_rw [Equiv.dvd_apply, Submonoid.coe_mul, ← Submonoid.mul_def, _root_.map_mul, hJ,
    inv_mul_eq_one, Nat.cast_mul, mul_comm s, eq_comm, and_comm, and_congr_left_iff]
  exact fun _ ↦
    (mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J))).symm

Goal state after:
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
⊢ (↑n * max 1 ‖A‖) ^ m * (↑B + 1) ^ m = ((↑n * max 1 ‖A‖) ^ e) ^ (↑n - ↑m) * (↑B + 1) ^ m

Tactic:
congr 1
        rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
          ← Real.rpow_natCast, div_mul_cancel₀]
        exact sub_ne_zero_of_ne (mod_cast hn.ne')

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)

Tactic:
by
  have hp : (1 : ℝ) < p :=
    mod_cast (is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin).one_lt
  exact ⟨-logb p (f p), neg_pos.mpr <| logb_neg hp hp0 hp1, by
    simpa using (rpow_logb (zero_lt_one.trans hp) hp.ne' hp0).symm⟩

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

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

Tactic:
simp [abs_add_le]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 < ‖(algebraMap ℚ_[p] (PadicAlgCl p)) x‖

Tactic:
PadicAlgCl.norm_extends

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 < ‖x‖
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
  -- Choose a clopen neighbourhood `V x` of each `x` contained in `U (r x)`.
  choose V hV hVx hVU using fun x ↦ compact_exists_isClopen_in_isOpen (U _).isOpen (hr x)
  -- Apply compactness to extract a finite subset of the `V`s which covers `X`.
  obtain ⟨t, ht⟩ : ∃ t, univ ⊆ ⋃ i ∈ t, V i :=
    isCompact_univ.elim_finite_subcover V (fun x ↦ (hV x).2) (fun x _ ↦ mem_iUnion.mpr ⟨x, hVx x⟩)
  -- Biject it noncanonically with `Fin n` for some `n`.
  refine ⟨_, fun j ↦ ⟨_, hV (t.equivFin.symm j)⟩, fun j ↦ ⟨_, hVU _⟩, fun x hx ↦ ?_⟩
  obtain ⟨m, hm, hm'⟩ := mem_iUnion₂.mp (ht hx)
  exact Set.mem_iUnion_of_mem (t.equivFin ⟨m, hm⟩) (by simpa)

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

Goal state before:
pp: K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
D : Type u_5
inst✝¹¹ : Field D
inst✝¹⁰ : Algebra D L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(stabilizer G P)) D L
⊢ IsDecompositionField K L P D

Tactic:
refine (isDecompositionField_iff K L P D).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_

Goal state after:
case refine_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 B
P : Ideal B
D : Type u_5
inst✝¹¹ : Field D
inst✝¹⁰ : Algebra D L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(stabilizer G P)) D L
⊢ ↥(stabilizer Gal(L/K) P) ≃* ↥(stabilizer G P)

case refine_2
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
D : Type u_5
inst✝¹¹ : Field D
inst✝¹⁰ : Algebra D L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(stabilizer G P)) D L
x✝ : ↥(stabilizer Gal(L/K) P)
x : L
⊢ ?refine_1 x✝ • x = x✝ • x
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: 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✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
⊢ Module.finrank D E = p.inertiaDegIn B

Tactic:
have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
  have := Module.finrank_mul_finrank K D E
  rwa [IsInertiaField.rank_right A K L P E hp, IsDecompositionField.rank_right A K L P D hp,
    mul_right_inj'] at this
  exact IsDedekindDomain.primesOver_ncard_ne_zero p B

Goal state after: