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

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1

Tactic:
rw [mersenne_coe_X] at w

Goal state after:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
hb : b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
ha : a✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
rcases hb with hb | hb

Goal state after:
case inl.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

case inl.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
hb : b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
ha : -a✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
rcases hb with hb | hb

Goal state after:
case inr.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

case inr.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case left
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ)
          (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤)).relIndex
      ⊤ ≠
    0

Tactic:
Subgroup.relIndex_top_right

Goal state after:
case left
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ) (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤)).index ≠
    0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ)
          ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) ⊤)).relIndex
      ⊤ ≠
    0

Tactic:
Subgroup.relIndex_top_right

Goal state after:
case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ)
        ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) ⊤)).index ≠
    0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
hG : DiscreteTopology ↥𝒢
H : Set (GL (Fin 2) R) := ↑𝒢 ∩ Set.range ⇑upperRightHom
hH : DiscreteTopology ↑H
x : R
hx : x ∈ ↑𝒢.strictPeriods
⊢ upperRightHom x ∈ H

Tactic:
by
    grind [SetLike.mem_coe, Subgroup.mem_strictPeriods_iff]

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
⊢ 0 < 𝒢.strictWidthInfty ↔ IsCusp ∞ 𝒢

Tactic:
constructor
  · refine fun h ↦ ⟨_, mem_strictPeriods_iff.mpr 𝒢.strictWidthInfty_mem_strictPeriods, ?_, ?_⟩
    · rw [GeneralLinearGroup.isParabolic_iff_of_upperTriangular (by simp)]
      simpa using h.ne'
    · simp [smul_infty_eq_self_iff]
  · -- Hard implication: if `∞` is a cusp, show the strict width is positive.
    rintro ⟨g, hgg, hgp, hgi⟩
    apply 𝒢.strictWidthInfty_nonneg.lt_of_ne'
    rw [← AddSubgroup.zmultiples_ne_bot]
    simp only [AddSubgroup.ne_bot_iff_exists_ne_zero, Subtype.exists, Ne, AddSubgroup.mk_eq_zero,
      exists_prop, and_comm, ← strictPeriods_eq_zmultiples_strictWidthInfty, mem_strictPeriods_iff]
    -- We have some `g ∈ 𝒢` which is parabolic and fixes `∞`. So `g = ±[1, x; 0, 1]` some `x ≠ 0`.
    rw [smul_infty_eq_self_iff] at hgi
    rw [Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular hgg hgi] at hgp
    rcases hgp with ⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩
    · -- If `g = [1, x; 0, 1]`, we're done
      exact ⟨x, hx, hgg⟩
    · -- If `g = -[1, x; 0, 1]` then `g ^ 2 = [1, 2 * x; 0, 1]`.
      exact ⟨2 • x, by grind,
        by simpa only [AddChar.map_nsmul_eq_pow, neg_sq] using pow_mem hgg 2⟩

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

Goal state before:
pp: case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)

Tactic:
rw [show x = g 0 1 by simpa using congr_arg (· 0 1) hx.symm]

Goal state after:
case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ ↑(↑g 0 1) ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: N : ℕ
⊢ (Subgroup.map (mapGL ℝ) Γ(N)).strictPeriods = AddSubgroup.zmultiples ↑N

Tactic:
by
  ext x
  have : AddSubgroup.zmultiples ↑N = .map (Int.castAddHom ℝ) (.zmultiples N) := by simp
  simp only [this, mem_strictPeriods_iff, Subgroup.mem_map, Gamma_mem]
  constructor
  · rintro ⟨g, ⟨-, hg, -, -⟩, hx⟩
    rw [show x = g 0 1 by simpa using congr_arg (· 0 1) hx.symm]
    apply AddSubgroup.mem_map_of_mem
    rwa [Int.mem_zmultiples_iff, ← ZMod.intCast_zmod_eq_zero_iff_dvd]
  · simp only [AddSubgroup.mem_map, AddSubgroup.mem_zmultiples_iff, existsAndEq, true_and,
      Units.ext_iff, mapGL_coe_matrix, map_apply_coe, forall_exists_index]
    refine fun a ha ↦ ⟨ModularGroup.T ^ (a * N), by simp [ModularGroup.coe_T_zpow], ?_⟩
    ext i j
    fin_cases i <;> fin_cases j <;> simp [ModularGroup.coe_T_zpow, ← ha]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
⊢ cuspFunction h f 0 = valueAtInfty f

Tactic:
refine (Tendsto.limUnder_eq ?_).symm
  have : (cuspFunction h f ∘ fun τ ↦ 𝕢 h τ : ℍ → ℂ) = f := by
    funext τ
    simpa using eq_cuspFunction τ hh.ne' hfper
  simpa [this] using hfanalytic.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)

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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 2) * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖

Tactic:
Subgroup.HasDetPlusMinusOne.abs_det hg,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖↑1 ^ (k - 2) * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
⊢ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Subgroup.closure {S, T}) =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}

Tactic:
MonoidHom.map_closure,

Goal state after:
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
⊢ Subgroup.closure (⇑(Matrix.SpecialLinearGroup.mapGL ℝ) '' {S, T}) =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ 1 < normSq ↑(T ^ n • z)

Tactic:
coe_T_zpow_smul_eq

Goal state after:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ 1 < normSq (↑z + ↑n)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ 9 * c ^ 4 ≤ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 =
    c ^ 4 * z.im ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 * 16

Tactic:
by grind [im_smul_eq_div_normSq]

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

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

Tactic:
tendsto_const_sub_iff

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

Goal state before:
pp: z : ℍ
⊢ e2Summand 0 z = 2 * riemannZeta 2

Tactic:
by
  simpa [e2Summand, eisSummand] using!
    (two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even (k := 2) (by grind) (by simp)).symm

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : ℤ → α
a : α
⊢ HasProd f a (symmetricIco ℤ) ↔ Tendsto (fun N ↦ ∏ n ∈ Ico (-↑N) ↑N, f n) atTop (𝓝 a)

Tactic:
by
  simp [HasProd, symmetricIco, ← Nat.map_cast_int_atTop, comp_def]

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

Goal state before:
pp: z : ℍ
⊢ 2 < 3

Tactic:
by linarith

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

Goal state before:
pp: case h
z : ℍ
⊢ Summable (Function.uncurry fun m n ↦ G2Term z ![m, n])

pp: case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]

pp: case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
· exact G2Term_prod_summable z

Goal state after:
case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]

case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem
γ g : SL(2, ℤ)
hg : g ∈ {S, T}
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
simp only [mem_insert_iff, mem_singleton_iff] at hg

Goal state after:
case mem
γ g : SL(2, ℤ)
hg : g = S ∨ g = T
⊢ G2 ∣[2] g = G2 - D2 g
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)
⊢ (E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑1 / ↑z)) * (↑π * I / 12) = 1 / ↑z / 2 + ↑π * I / 12 * E2 z

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

Tactic:
· field_simp
    grind [I_sq]

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)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = ↑z ^ (-1 / 2) / 2 * (↑z ^ 2⁻¹)⁻¹ + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: ⊢ bernoulli 4 = -1 / 30

Tactic:
decide +kernel

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

Goal state before:
pp: ⊢ bernoulli 6 = 1 / 42

Tactic:
decide +kernel

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

Goal state before:
pp: z : ℍ
⊢ E2 z = 1 - 24 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
simp [E2, G2_eq_tsum_cexp, riemannZeta_two]

Goal state after:
z : ℍ
⊢ 6 / ↑π ^ 2 * 2⁻¹ * (2 * (↑π ^ 2 / 6) - 8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n) =
    1 - 24 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: τ : ℍ
⊢ HasSum (fun m ↦ ?m.5 m • Function.Periodic.qParam 1 ↑τ ^ m) (E2 τ)

Tactic:
simpa only [Function.Periodic.qParam, ofReal_one, div_one] using hasSum_qExpansion_E2 (z := τ)

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n y : ℤ
⊢ eisSummand ↑k ![(-n, -y).1, (-n, -y).2] z = eisSummand ↑k ![(n, y).1, (n, y).2] z

Tactic:
by simp [eisSummand, ← neg_add _ (y : ℂ), -neg_add_rev, hk2.neg_pow]

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ?m.161 ∈ integerComplement

Tactic:
by simpa using z.int_div_mem_integerComplement (n := -d) (by aesop)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ IsClosed 𝒟

Tactic:
refine .inter (.preimage (by fun_prop) isClosed_Ici) ?_

Goal state after:
⊢ IsClosed fun z ↦ Real.le✝ |z.re| (1 / 2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hf
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ { coe := ↑x + ↑↑t * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)

Tactic:
refine .mono_left ?_ nhdsWithin_le_nhds
    simpa [show 𝓝 (x : ℂ) = 𝓝 (x + (((0 : ℝ≥0) : ℝ) : ℂ) * Complex.I) by simp,
      isOpenEmbedding_coe.tendsto_nhds_iff] using! Continuous.tendsto (by fun_prop) _

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ jacobiTheta τ

Tactic:
by
  simp_rw [funext jacobiTheta_eq_jacobiTheta₂]
  exact differentiableAt_jacobiTheta₂_snd 0 hτ

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)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (Subgroup.toAddSubgroup
            (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (Set.range (⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))).index ≠
      0

Tactic:
MonoidHom.map_closure,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (Subgroup.toAddSubgroup (Subgroup.closure (⇑(QuotientGroup.mk' (torsion K)) '' Set.range u)))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (Set.range (⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))).index ≠
      0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ logMap (c • x) = logMap x

Tactic:
have : mixedEmbedding.norm (c • (1 : mixedSpace K)) ≠ 0 := by
    rw [norm_smul, map_one, mul_one]
    exact pow_ne_zero _ (abs_ne_zero.mpr hc)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
this : mixedEmbedding.norm (c • 1) ≠ 0
⊢ logMap (c • x) = logMap x
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
⊢ u ∈ realUnits K ↔ ∃ v, (algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v = ↑u

Tactic:
by
  simp [realUnits, MonoidHom.mem_range, RingHom.toMonoidHom_eq_coe, Units.ext_iff]

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)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ζ = 1

Tactic:
mul_eq_right₀,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ = 1
⊢ ζ = 1

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ↑(preimageOfMemIntegerSet a) ≠ 0
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ regulator K / regulator ↥K⁺ = 2 ^ rank K / 2 ^ rank K * (regulator K / regulator ↥K⁺)

Tactic:
div_self (by positivity),

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ regulator K / regulator ↥K⁺ = 1 * (regulator K / regulator ↥K⁺)
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
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
⊢ 1 * 2 = w.mult

Tactic:
h.isComplex.mult_eq_two,

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
⊢ 1 * 2 = 2
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
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
⊢ Module.finrank (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}) =
    Module.finrank (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})

Tactic:
refine Algebra.finrank_eq_of_equiv_equiv (Int.quotientSpanNatEquivZMod p) ?_ (by ext; simp)

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
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
⊢ 𝓞 K ⧸ span {↑p, (aeval θ) Q} ≃+* (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: case refine_2
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)
this : root P ^ (p ^ f) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = root P
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = ↑1

Tactic:
Units.val_one,

Goal state after:
case refine_2
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)
this : root P ^ (p ^ f) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = root P
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
⊢ normAtAllPlaces '' normAtAllPlaces ⁻¹' ↑expMapBasis '' s = ↑expMapBasis '' s

Tactic:
apply normAtAllPlaces_image_preimage_of_nonneg

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
⊢ ∀ x ∈ ↑expMapBasis '' s, ∀ (w : InfinitePlace K), 0 ≤ x w
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n✝ j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hj_Unit : IsUnit ↑j
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
⊢ 2 ≤ n + 2

Tactic:
by linarith

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✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this✝ : NeZero ↑n
hP : P ∈ normalizedFactors (cyclotomic n K)
this : {P, P} ≤ normalizedFactors (cyclotomic n K)
⊢ P * P ∣ cyclotomic n K

Tactic:
have := prod_dvd_prod_of_le 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✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this✝¹ : NeZero ↑n
hP : P ∈ normalizedFactors (cyclotomic n K)
this✝ : {P, P} ≤ normalizedFactors (cyclotomic n K)
this : {P, P}.prod ∣ (normalizedFactors (cyclotomic n K)).prod
⊢ P * P ∣ cyclotomic n K
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)ˣ
⊢ ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex ⊤) = ↑(Subgroup.closure (Set.range u) ⊔ torsion K).index

Tactic:
Subgroup.relIndex_top_right

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ ↑(Subgroup.closure (Set.range u) ⊔ torsion K).index = ↑(Subgroup.closure (Set.range u) ⊔ torsion K).index