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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ Tendsto (fun m ↦ ∑' (n : ℕ+), r ^ (↑n * ↑m)) atTop (𝓝 0)

Tactic:
have h1 (m : ℕ+) : ‖r ^ (m : ℕ)‖ < 1 := by
    rwa [norm_pow, pow_lt_one_iff_of_nonneg (norm_nonneg _) (NeZero.ne _)]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ ↑m‖ < 1
⊢ Tendsto (fun m ↦ ∑' (n : ℕ+), r ^ (↑n * ↑m)) atTop (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)) =O[atTop] fun n ↦ ↑n ^ k

Tactic:
simp only [← Real.rpow_intCast]
  apply qExpansion_coeff_isBigO_of_norm_isBigO
  obtain ⟨C, hC⟩ := exists_bound hk f
  simp_rw [IsBigO, ← Int.cast_neg, Real.rpow_intCast, IsBigOWith, eventually_comap]
  use C
  filter_upwards [eventually_le_nhds zero_lt_one] with _ hτ τ rfl
  refine (hC τ).trans (le_of_eq ?_)
  rw [max_eq_right, zpow_neg, Real.norm_of_nonneg (by positivity), one_div]
  exact one_le_one_div (by positivity) (zpow_le_one₀ τ.im_pos hτ hk)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑(↑g 0 0)| - |(-z.re)| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
abs_neg,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑(↑g 0 0)| - |z.re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: α : Type u_1
f : ℤ → α
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
a : α
hf : HasProd f a (symmetricIcc ℤ)
hf2 : Tendsto (fun N ↦ (f ↑N)⁻¹) atTop (𝓝 1)
⊢ HasProd f a (symmetricIco ℤ)

Tactic:
simp only [HasProd, tendsto_map'_iff, symmetricIcc_eq_map_Icc_nat,
    ← Nat.map_cast_int_atTop, symmetricIco] at *

Goal state after:
α : Type u_1
f : ℤ → α
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
a : α
hf2 : Tendsto (fun N ↦ (f ↑N)⁻¹) atTop (𝓝 1)
hf : Tendsto ((fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Icc (-↑N) ↑N) atTop (𝓝 a)
⊢ Tendsto (((fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Ico (-N) N) ∘ Nat.cast) atTop (𝓝 a)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ S • T • ρ = ρ

Tactic:
← SL_neg_smul S,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ -S • T • ρ = ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝¹ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this : S • ρ = T • ρ
⊢ S • T⁻¹ • (1 +ᵥ ρ) = 1 +ᵥ ρ

Tactic:
← SL_neg_smul S,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝¹ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this : S • ρ = T • ρ
⊢ -S • T⁻¹ • (1 +ᵥ ρ) = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)) atTop
    (𝓝 (-8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n))

Tactic:
have : -8 * π ^ 2 * ∑' n : ℕ+, σ 1 n * 𝕢 z ^ (n : ℕ) =
      ∑' m : ℕ, (-8 * π ^ 2 * ∑' n : ℕ+, n * 𝕢 z ^ ((m + 1) * n)) := by
    have := tsum_prod_pow_eq_tsum_sigma 1 (norm_exp_two_pi_I_lt_one z)
    rw [tsum_pnat_eq_tsum_succ (f := fun d ↦ ∑' c : ℕ+, c ^ 1 * 𝕢 z ^ (d * c : ℕ))] at this
    simp [← tsum_mul_left, ← this]

Goal state after:
z : ℍ
this :
  -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
⊢ Tendsto (fun N ↦ ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)) atTop
    (𝓝 (-8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
levelOne_odd_weight_rank_zero hk_odd

Goal state after:
case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ 0 < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

Tactic:
← mcast_eq_zero_iff (b := ↑(k - 12)) (by lia) rfl

Goal state after:
case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯ = 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 1 < normSq ↑x

Tactic:
rw [one_lt_normSq_iff, ← Set.mem_Ioi, ← interior_Ici]

Goal state after:
case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ ‖↑x‖ ∈ interior (Set.Ici 1)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hc_eq : c = 1728
⊢ 1728 * discriminant z = E₄ z ^ 3 - E₆ z ^ 2

Tactic:
← hc_eq,

Goal state after:
z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hc_eq : c = 1728
⊢ c * discriminant z = E₄ z ^ 3 - E₆ z ^ 2
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ∏ q, quotientFunc f q = 0
⊢ ∀ i ∈ Finset.univ, MDiff (quotientFunc f i)

Tactic:
· exact Quotient.forall.mpr fun r _ ↦ (translate f r.val⁻¹).holo'

Goal state after:
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
t : ℝ
ht : 0 < t
⊢ 0 < (I * ↑t⁻¹).im

Tactic:
simpa

Goal state after:
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
t : ℝ
ht : 0 < t
⊢ 0 < (I * ↑t).im

Tactic:
simpa

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ 1 + emultiplicity (↑p) (x - y) = emultiplicity (↑p) (x - y) + 1

Tactic:
add_comm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (x - y) + 1 = emultiplicity (↑p) (x - y) + 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Tactic:
rw [Nat.prime_iff_prime_int] at hp

Goal state after:
case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 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)
p : ι → Prop
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), p i → ↑f i ∈ A i}

Tactic:
topologicalSpace_eq_iSup cofinite,

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)
p : ι → Prop
⊢ IsOpen[⨆ S, ⨆ (hS : cofinite ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))]
    {f | ∀ (i : ι), p i → ↑f i ∈ A i}
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)
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), ↑f i ∈ A i}

Tactic:
topologicalSpace_eq_iSup cofinite,

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)
⊢ IsOpen[⨆ S, ⨆ (hS : cofinite ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))]
    {f | ∀ (i : ι), ↑f i ∈ A i}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

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

Tactic:
refine measurable_fst.prodMk <| Measurable.comp ?_ measurable_snd

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(OpenPartialHomeomorph.pi fun x ↦ polarCoord).symm
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < x.1 w

Tactic:
← this

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < a.1 w
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
this : (powMonoidHom 2).range.index = 2
⊢ (powMonoidHom 2).range ≤ (unitsMulComplexConjInv K).range

Tactic:
rintro _ ⟨ζ, _, rfl⟩

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (powMonoidHom 2).range.index = 2
ζ : ↥(torsion K)
⊢ (powMonoidHom 2) ζ ∈ (unitsMulComplexConjInv K).range
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
⊢ (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1

Tactic:
refine ⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ : ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
u : (𝓞 K)ˣ
hu : Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
⊢ ⊤ ≤ (unitsMulComplexConjInv K).range

case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h : (unitsMulComplexConjInv K).range.index = 1
⊢ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J

Tactic:
simp_rw [idealSetMap, ← hx₂, preimageOfMemIntegerSet_mixedEmbedding]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ x ∈ ↑↑J
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
i w : { w // w ≠ w₀ }
⊢ ↑((equivInfinitePlace K).symm ↑w).mult *
      Real.log
        (((equivInfinitePlace K).symm ↑w)
          ((algebraMap (↥K⁺) K) ↑↑(fundSystem (↥K⁺) ((finCongr ⋯) (g.symm (f.symm i)))))) =
    2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i w

Tactic:
equivInfinitePlace_symm_apply

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
i w : { w // w ≠ w₀ }
⊢ ↑((equivInfinitePlace K).symm ↑w).mult * Real.log (↑w ↑↑(fundSystem (↥K⁺) ((finCongr ⋯) (g.symm (f.symm i))))) =
    2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i w
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
hv : v = w.comap (algebraMap K L)
h : IsUnramified K w
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult

pp: 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

Tactic:
· rw [h.finrank_eq_one v, hv, h.eq, mul_one]

Goal state after:
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.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
inst✝¹ : NumberField K
inst✝ : NumberField L
⊢ #(ramifiedPlacesOver L v).toFinset • 2 + ∑ x ∈ (unramifiedPlacesOver L v).toFinset, 1 = Module.finrank K L

Tactic:
add_comm

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
⊢ ∑ x ∈ (unramifiedPlacesOver L v).toFinset, 1 + #(ramifiedPlacesOver L v).toFinset • 2 = Module.finrank K L
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ 1) ⋯)

Tactic:
simpa

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
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
m : ℕ
hm : j * m % (n + 2) = 1
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
use ∑ i ∈ range m, (ζ ^ j) ^ i

Goal state after:
case h
n✝ j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
m : ℕ
hm : j * m % (n + 2) = 1
⊢ ζ - 1 = (ζ ^ j - 1) * ∑ i ∈ range m, (ζ ^ j) ^ i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : x ∈ ↑expMapBasis '' closure (paramSet K)
⊢ x ∈ compactSet K

Tactic:
simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
  obtain ⟨y, hy, rfl⟩ := hx₁
  refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
  · exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))
  · split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (normLeOne K) = 2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral (normLeOne_eq_preimage_image K).symm
    (measurableSet_normLeOne K), normLeOne_eq_preimage,
    normAtAllPlaces_image_preimage_expMapBasis,
    setLIntegral_expMapBasis_image (measurableSet_paramSet K) (by fun_prop)]
  simp_rw [ENNReal.inv_mul_cancel_right
    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
    (prod_ne_top fun _ _ ↦ ofReal_ne_top)]
  rw [setLIntegral_paramSet_exp K Module.finrank_pos, ofReal_mul zero_le_two, mul_pow,
    ofReal_ofNat, ENNReal.mul_inv_cancel_right (Nat.cast_ne_zero.mpr Module.finrank_pos.ne')
    (natCast_ne_top _), coe_nnreal_eq, NNReal.coe_real_pi, mul_mul_mul_comm, ← ENNReal.inv_pow,
    ← mul_assoc, ← mul_assoc, ENNReal.inv_mul_cancel_right (pow_ne_zero _ two_ne_zero)
    (pow_ne_top ENNReal.ofNat_ne_top)]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K)

Tactic:
exact mul_pos (mul_pos (by positivity) (regulator_pos K)) (Nat.cast_pos.mpr (classNumber_pos K))

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

Goal state before:
pp: case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    (2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)

Tactic:
ENNReal.toReal_mul,

Goal state after:
case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    (2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K).toReal * (ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)