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

Goal state before:
pp: case h₂
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ C * ‖{ coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }.im ^ (-e)‖ ≤ C * ↑n ^ e

Tactic:
simp [← UpperHalfPlane.coe_im, Real.rpow_neg_eq_inv_rpow, hne]

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

Goal state before:
pp: case hg
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))

Tactic:
· exact summable_zero.congr
      fun b ↦ by simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]

Goal state after:
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
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)
⊢ normSq ↑z = 1 ∧ z.re = 1 / 2

Tactic:
have : 1 ≤ normSq z := hz.1
    have : 0 ≤ -2 * z.re + 1 := by linarith [(le_abs_self _).trans hz.2]
    constructor <;> linarith

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

Goal state before:
pp: case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
· simpa only [h2, D2_T, sub_zero] using G2_T_transform

Goal state after:
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 • ρ
⊢ T • ρ = 1 +ᵥ ρ

Tactic:
modular_T_smul

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 • ρ
⊢ 1 +ᵥ ρ = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ serreDerivative k (F + G) = serreDerivative k F + serreDerivative k G

Tactic:
ext z
  simp [serreDerivative, normalizedDerivOfComplex_add F G hF hG]
  ring_nf

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g • z).im = z.im

Tactic:
rw [← this (g := g⁻¹) hg (by simpa using hz) (by simpa using le_of_not_ge hden)]

Goal state after:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g⁻¹ • g • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = deriv sqrt ↑z / (↑z).sqrt + logDeriv η ↑z

Tactic:
deriv_sqrt (mem_slitPlane z),

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = ↑z ^ (-1 / 2) / 2 / (↑z).sqrt + logDeriv η ↑z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), 1 / (↑↑b * ↑z + ↑n) ^ (k - 1 + 1) =
      (-2 * ↑π * I) ^ (k - 1 + 1) / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (c : ℤ), eisSummand ↑k ![(0, c).1, (0, c).2] z +
      2 • ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
show k - 1 + 1 = k by grind,

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), 1 / (↑↑b * ↑z + ↑n) ^ k =
      (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (c : ℤ), eisSummand ↑k ![(0, c).1, (0, c).2] z +
      2 • ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
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
⊢ mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯ = 0

Tactic:
refine ih (k - 12) (by lia) ?_

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
⊢ ↑((k - 12) / 12) < (qExpansion 1 ⇑(mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯)).order
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℤ
z : ℍ
n : ℕ
v : ↑(gammaSet 1 n 0)
⊢ (↑(↑v 0) * ↑z + ↑(↑v 1)) ^ (-k) = (↑n ^ k)⁻¹ * (↑(divIntMap (↑n) (↑v) 0) * ↑z + ↑(divIntMap (↑n) (↑v) 1)) ^ (-k)

Tactic:
gammaSet_eq_gcd_mul_divIntMap v.2

Goal state after:
k : ℤ
z : ℍ
n : ℕ
v : ↑(gammaSet 1 n 0)
⊢ (↑((n • divIntMap ↑n ↑v) 0) * ↑z + ↑((n • divIntMap ↑n ↑v) 1)) ^ (-k) =
    (↑n ^ k)⁻¹ * (↑(divIntMap (↑n) (↑v) 0) * ↑z + ↑(divIntMap (↑n) (↑v) 1)) ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n ↦ cexp (↑π * I * ↑(n + 1) ^ 2 * τ) * 2) (jacobiTheta τ + 1 - 1 * 2)
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
add_sub_assoc,

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n ↦ cexp (↑π * I * ↑(n + 1) ^ 2 * τ) * 2) (jacobiTheta τ + (1 - 1 * 2))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
⊢ 1 ≤ k

Tactic:
by omega

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

Goal state before:
pp: 𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ

Tactic:
have : ProperlyDiscontinuousSMul 𝒮ℒ' ℍ := inferInstance

Goal state after:
𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
this : ProperlyDiscontinuousSMul ↥𝒮ℒ' ℍ
⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ
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 : ∃ i ∈ Finset.univ, quotientFunc f i = 0
⊢ ⇑f = 0

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:
· simpa [QuotientGroup.exists_mk] using hf

Goal state after:
𝒢 ℋ : 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)
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)
n : ℕ
p : ℂ
⊢ ↑(2 * ↑n) ^ s / ↑(h Γ) ^ s = ↑2 ^ s * ↑↑n ^ s / ↑(h Γ) ^ s

Tactic:
ofReal_mul,

Goal state after:
Γ : 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)
n : ℕ
p : ℂ
⊢ (↑2 * ↑↑n) ^ s / ↑(h Γ) ^ s = ↑2 ^ s * ↑↑n ^ s / ↑(h Γ) ^ s
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ ((fun w ↦ x✝.1 ↑w, fun w ↦ (x✝.1 ↑w, x✝.2 w)) ∈ Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π

Tactic:
Set.mem_prod,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ ((fun w ↦ x✝.1 ↑w) ∈ Set.univ ∧ (fun w ↦ (x✝.1 ↑w, x✝.2 w)) ∈ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    (x✝.1 ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ∧ x✝.2 ∈ Set.univ.pi fun x ↦ Set.Ioo (-π) π
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

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

Tactic:
Set.mem_prod,

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
⊢ c • x ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : c • x ∈ fundamentalCone K
⊢ x ∈ fundamentalCone K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ Submodule.span ℤ (Set.range ⇑B)

Tactic:
rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
    exact ⟨u, trivial, rfl⟩

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
u : (𝓞 K)ˣ
⊢ (∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u) ↔ ∃ v, ↑((algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v) = ↑↑u

Tactic:
IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) K

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

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

Tactic:
refine this ▸ Subgroup.index_dvd_of_le ?_
    rintro _ ⟨ζ, _, rfl⟩
    exact ⟨ζ, Subtype.ext_iff.mpr (by simp [pow_two])⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // mixedEmbedding.norm ↑a = ↑i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }

Tactic:
by
        simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]
        rfl

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)
⊢ |(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:
let f : Fin (rank K + 1) ≃ InfinitePlace K :=
    (finSuccEquiv _).trans ((Equiv.optionSubtype _).symm e₁.symm).val
  -- And `g` corresponds to the restriction of `f⁻¹` to `{w // w ≠ w₂}`
  let g : {w // w ≠ w₂} ≃ Fin (rank K) :=
    (Equiv.subtypeEquiv f.symm (fun _ ↦ by simp [f])).trans
      (finSuccAboveEquiv (f.symm w₂)).symm
  have h_col := congr_arg abs <| det_permute (g.trans e₂.symm)
    (of fun i w : {w // w ≠ w₂} ↦ (mult w.val : ℝ) * (w.val (u (e₂ i) : K)).log)
  rw [abs_mul, ← Int.cast_abs, Equiv.Perm.sign_abs, Int.cast_one, one_mul] at h_col
  rw [← h_col]
  have h := congr_arg abs <| submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det'
    (of fun i w ↦ (mult (f w) : ℝ) * ((f w) (u i)).log) ?_ 0 (f.symm w₂)
  · rw [← det_reindex_self e₁, ← det_reindex_self g]
    · rw [Units.smul_def, abs_zsmul, Int.abs_negOnePow, one_smul] at h
      convert! h
      · ext; simp only [ne_eq, reindex_apply, submatrix_apply, of_apply, Equiv.apply_symm_apply,
          Equiv.trans_apply, Fin.succAbove_zero, id_eq, finSuccEquiv_succ,
          Equiv.optionSubtype_symm_apply_apply_coe, f]
      · ext; simp only [ne_eq, Equiv.coe_trans, reindex_apply, submatrix_apply, Function.comp_apply,
          Equiv.apply_symm_apply, id_eq, of_apply]; rfl
  · intro _
    simp_rw [of_apply, ← Real.log_pow]
    rw [← Real.log_prod, Equiv.prod_comp f (fun w ↦ (w (u _) ^ (mult w))), prod_eq_abs_norm,
      Units.norm, Rat.cast_one, Real.log_one]
    exact fun _ _ ↦ pow_ne_zero _ <| (map_ne_zero _).mpr (coe_ne_zero _)

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
hσ₂ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
⊢ IsCMField K

Tactic:
exact IsCMField.of_forall_isConj K hσ₂

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : (Multiset.map natDegree (normalizedFactors (cyclotomic n K))).sum = φ n
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
map_congr rfl this

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : (Multiset.map (fun x ↦ orderOf (unitOfCoprime (p ^ f) ⋯)) (normalizedFactors (cyclotomic n K))).sum = φ n
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
⊢ Associated (ζ - 1) (σ (ζ - 1))

Tactic:
by
  rw [map_sub, map_one, ← hζ.autToPow_spec R σ]
  apply hζ.associated_sub_one_pow_sub_one_of_coprime
  exact ZMod.val_coe_unit_coprime ((autToPow R hζ) σ)

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
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : ↑((I.rootsOfUnityMapQuot n) ⟨ζ, hζ✝⟩) = ↑1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := ↑↑ζ
hμ : IsPrimitiveRoot μ t
⊢ False

Tactic:
rootsOfUnityMapQuot_apply,

Goal state after:
K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (Quotient.mk I) ↑ζ = ↑1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := ↑↑ζ
hμ : IsPrimitiveRoot μ t
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : mixedSpace K
ha : a ∈ fundamentalCone K
right✝ : a ∈ {x | mixedEmbedding.norm x ≤ 1}
hx : ¬∀ (w : InfinitePlace K), 0 < normAtAllPlaces a w
⊢ normAtAllPlaces a ∈ ↑expMapBasis '' paramSet K

Tactic:
exact (hx fun w ↦ fundamentalCone.normAtPlace_pos_of_mem ha w).elim

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

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

Tactic:
rw [normLeOne_eq_preimage]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K) ⊆ interior (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (normLeOne K) ⊆ normAtAllPlaces ⁻¹' compactSet K

Tactic:
rw [normLeOne_eq_preimage]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K) ⊆ normAtAllPlaces ⁻¹' compactSet K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
rw [normLeOne_eq_preimage]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsBounded (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K)
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ¬∃ δ, HasDirichletDensity S δ
⊢ 0 ≤ 0

Tactic:
exact le_rfl

Goal state after:
Module: Mathlib.RingTheory.Unramified.Dedekind

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : p.IsMaximal
⊢ Submodule.IsPrincipal q'

Tactic:
let : Field (A ⧸ p) := Ideal.Quotient.field p

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this✝ : p.IsMaximal
this : Field (A ⧸ p) := Ideal.Quotient.field p
⊢ Submodule.IsPrincipal q'
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
hs : ∀ (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a k' l.1 * (newBasis K) l.2)) b) = 0 (k', b)
l : β
b b' : K →+* ℂ
⊢ ((newBasis K).repr (a k' l * (newBasis K) b)) b' = 0 b'

Tactic:
specialize hs b'

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
l : β
b b' : K →+* ℂ
hs : (fun l ↦ ((newBasis K).repr (a k' l.1 * (newBasis K) l.2)) b') = 0 (k', b')
⊢ ((newBasis K).repr (a k' l * (newBasis K) b)) b' = 0 b'
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
⊢ a * b ≠ 0

Tactic:
by omega

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

Goal state before:
pp: case e_f.e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r✝ : K →+* ℂ
r : β
⊢ ∑ x_1, ↑(a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (newBasis K) x_1 =
    ↑(x (r, r✝)) * ∑ u, ↑(a' K a k r r✝ u) * (newBasis K) u

Tactic:
rw [mul_sum]

Goal state after:
case e_f.e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r✝ : K →+* ℂ
r : β
⊢ ∑ x_1, ↑(a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (newBasis K) x_1 =
    ∑ i, ↑(x (r, r✝)) * (↑(a' K a k r r✝ i) * (newBasis K) i)
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
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ i + 1 ≤ p ^ t

Tactic:
by omega

Goal state after: