mathlib-initiative/mathlib-tactics huggingface dataset:
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:
conv =>

Goal state after:
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') τ‖‖
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case mp
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ qExpansion h f = 0 → f = 0

pp: case mpr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ f = 0 → qExpansion h f = 0

Tactic:
· intro H
    ext z
    simp [← (hasSum_qExpansion hh hfper hfhol hfbdd z).tsum_eq, H]

Goal state after:
case mpr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ f = 0 → qExpansion h f = 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case succ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n
⊢ qExpansion h ⇑(f.pow n) * qExpansion h ⇑f = qExpansion h ⇑f ^ (n + 1)

Tactic:
ih,

Goal state after:
case succ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n
⊢ qExpansion h ⇑f ^ n * qExpansion h ⇑f = qExpansion h ⇑f ^ (n + 1)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < ↑t
⊢ max (↑t) (1 / ↑t) ^ ↑k / ‖↑↑t ^ ↑k‖ = max 1 (1 / ↑t ^ ↑k) ^ 2

Tactic:
rw [← coe_nnnorm]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < ↑t
⊢ max (↑t) (1 / ↑t) ^ ↑k / ↑‖↑↑t ^ ↑k‖₊ = max 1 (1 / ↑t ^ ↑k) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
⊢ ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z ^ 2 / denom (toGL (φ A) * toGL (φ B)) ↑z =
    ↑(↑A 1 0) / denom (toGL (φ A)) ↑(toGL (φ B) • z) + denom (toGL (φ B)) ↑z * ↑(↑B 1 0)

Tactic:
simp only [pow_two, ← mul_assoc, denom_cocycle A B z.im_ne_zero, this,
    ModularGroup.sl_moeb, ← hd]

Goal state after:
A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
⊢ ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z * denom (toGL (φ B)) ↑z /
      (denom (toGL (φ A)) ↑(toGL (φ B) • z) * denom (toGL (φ B)) ↑z) =
    (↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z -
          ↑(↑B 1 0) * denom (toGL (φ A)) ↑(toGL (φ B) • z) * denom (toGL (φ B)) ↑z) /
        denom (toGL (φ A)) ↑(toGL (φ B) • z) +
      denom (toGL (φ B)) ↑z * ↑(↑B 1 0)
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⁻¹ * S
hSre : (S • z).re = -z.re
h : ↑g 0 0 = -1
this : |↑(-1) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ ‖↑z‖ = ‖↑ρ‖

Tactic:
by rw [hz', norm_ρ]

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

Goal state before:
pp: case e'_5
z : ℂ
hz : z ∈ ℍₒ
this :
  Summable fun n ↦ ↑n ^ 1 * 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ n / (1 - 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ n)
⊢ (fun i ↦ logDeriv (fun x ↦ 1 - eta_q i x) z) = fun i ↦
    -2 * ↑π * I *
      (↑(i + 1) ^ 1 * 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ (i + 1) /
        (1 - 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ (i + 1)))

Tactic:
grind [one_sub_eta_logDeriv_eq]

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).det = 1
⊢ ↑g 0 1 = -↑g 0 0 - 1

Tactic:
simp_rw [det_fin_two] at this

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
this : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0 = 1
⊢ ↑g 0 1 = -↑g 0 0 - 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑' (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))

pp: case hf
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑' (n : ℤ), G2Term z ![m, n]

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:
· rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]
    · congr with a
      rw [e2Summand, tsum_eq_of_summable_unconditional
        (summable_right_one_div_linear_sub_one_div_linear_succ z a), ← Summable.tsum_add
        ((G2Term_prod_summable z).prod_factor _)
        (summable_right_one_div_linear_sub_one_div_linear_succ z a)]
      exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])
    · simpa only [tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z, add_zero]
        using (G2Term_prod_summable z).prod

Goal state after:
case hf
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑' (n : ℤ), G2Term z ![m, n]

case hg
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.Derivative

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

Tactic:
ext z
  have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
  have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
  simp only [normalizedDerivOfComplex, Pi.add_apply, Pi.mul_apply]
  rw [show (F * G) ∘ ofComplex = (F ∘ ofComplex) * (G ∘ ofComplex) from rfl,
    deriv_mul hFz hGz]
  simp [Function.comp_apply, ofComplex_apply]
  ring

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * ↑(↑g).det ^ (k + 2 - 1) * denom g ↑z ^ (-(k + 2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))

Tactic:
show k + 2 - 1 = (k - 1) + 2 by ring,

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * ↑(↑g).det ^ (k - 1 + 2) * denom g ↑z ^ (-(k + 2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case pos
q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : q = 0
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q

Tactic:
simpa [hq0] using! Periodic.cuspFunction_zero_of_zero_at_inf one_pos
      discriminant_isZeroAtImInfty.zero_at_infty_comp_ofComplex

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

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
⊢ SummableLocallyUniformlyOn (fun n ↦ f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) ℍₒ

Tactic:
by
  apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
  intro K hK hKc
  have : CompactSpace K := isCompact_univ_iff.mp (isCompact_iff_isCompact_univ.mp hKc)
  let c : ContinuousMap K ℂ := ⟨fun r : K ↦ Complex.exp (2 * π * I * r / p), by fun_prop⟩
  let r : ℝ := ‖mkOfCompact c‖
  have hr : ‖r‖ < 1 := by
    simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
      ContinuousMap.coe_mk, c]
    intro x
    have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by
      ring_nf
    simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩
  refine ⟨_, by simpa using (summable_norm_mul_geometric_of_norm_lt_one' hr
    (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf))), fun n z hz ↦ ?_⟩
  have h0 := pow_le_pow_left₀ (norm_nonneg _) (norm_coe_le_norm (mkOfCompact c) ⟨z, hz⟩) n
  simp only [norm_mkOfCompact, mkOfCompact_apply, ContinuousMap.coe_mk, ← exp_nsmul', Pi.smul_apply,
    iteratedDerivWithin_cexp_aux k n p isOpen_upperHalfPlaneSet (hK hz), smul_eq_mul,
    norm_mul, norm_pow, Complex.norm_div, norm_ofNat, norm_real, Real.norm_eq_abs, norm_I, mul_one,
    norm_natCast, abs_norm, ge_iff_le, r, c] at *
  rw [← mul_assoc]
  gcongr
  convert! h0
  rw [← norm_pow, ← exp_nsmul']

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

Goal state before:
pp: case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h : Submodule.Quotient.mk (E hk) = 0
hE : (PowerSeries.coeff 0) (qExpansion 1 ⇑(E hk)) = 1
⊢ False

Tactic:
Submodule.Quotient.mk_eq_zero

Goal state after:
case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h : E hk ∈ cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
hE : (PowerSeries.coeff 0) (qExpansion 1 ⇑(E hk)) = 1
⊢ False
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ (-2 * ↑π * I) ^ (k + 1) / ↑k ! *
      (↑0 ^ k * cexp (2 * ↑π * I * ↑z) ^ 0 + ∑' (n : ℕ+), ↑↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ ↑n) =
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * ∑' (n : ℕ+), ↑↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ ↑n

pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
· simp [show k ≠ 0 by grind]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ |z.re| ≤ |1 / 2|

Tactic:
abs_of_pos <| one_half_pos (α := ℝ)

Goal state after:
case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ |z.re| ≤ 1 / 2
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: case hp
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed {x | ↑((extensionEmbeddingOfIsReal hv) x) = (extensionEmbedding v) x}

Tactic:
exact isClosed_eq
      (Complex.continuous_ofReal.comp (isometry_extensionEmbeddingOfIsReal hv).continuous)
      (isometry_extensionEmbedding v).continuous

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝ : (i : ι) → TopologicalSpace (R i)
⊢ topologicalSpace R A 𝓕 =
    ⨆ S,
      ⨆ (x : 𝓕 ≤ 𝓟 S),
        TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced DFunLike.coe inferInstance)

Tactic:
topologicalSpace

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁵ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝⁴ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝⁴ i] ↑(B i))
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousSMul G (R i)
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite] fun p ↦ p.1 • p.2

Tactic:
continuous_dom_prod_left hBopen.out

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁵ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝⁴ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝⁴ i] ↑(B i))
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousSMul G (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite]
      ((fun p ↦ p.1 • p.2) ∘ Prod.map id (inclusion R (fun i ↦ ↑(B i)) hS))
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)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
this : IsUnit y
⊢ ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u

Tactic:
exact ⟨this.unit, by simp [hy]⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ ζ, ζ • a = b

Tactic:
integerSetToAssociates_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ ⟦preimageOfMemIntegerSet a⟧ = ⟦preimageOfMemIntegerSet b⟧ ↔ ∃ ζ, ζ • a = b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inl
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 // ⟨absNorm ↑↑a.1, ⋯⟩ = ⟨i, hi⟩ } ≃ { b // ⟨intNorm ↑((idealSetEquiv K J) ↑b), ⋯⟩ = ⟨i, hi⟩ }

Tactic:
Subtype.mk.injEq

Goal state after:
case inl
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 // absNorm ↑↑a.1 = i } ≃ { b // intNorm ↑((idealSetEquiv K J) ↑b) = i }
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:
simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]

Goal state after:
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 // intNorm ↑((idealSetEquiv K J) a) = i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
f : ι → realSpace K
⊢ ↑expMap (∑ i ∈ s, f i) = ∏ i ∈ s, ↑expMap (f i)

Tactic:
ext
  simp [← Real.exp_sum, ← mul_sum]

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 : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm) Q ∈
    {d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ))}

Tactic:
rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]
          exact ((primesOverSpanEquivMonicFactorsModAux _).symm ⟨Q, hQ⟩).prop

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:
rw [← mem_primesOver_iff_mem_normalizedFactors _ (by simp [NeZero.ne p])]
      exact ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).coe_prop

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
key : ↑n = ∑ i ∈ range n, (1 - ζ ^ i)
i : ℕ
x✝ : i ∈ range n
h : ζ - 1 ∣ -(ζ ^ i - 1)
⊢ ζ - 1 ∣ 1 - ζ ^ i

Tactic:
neg_sub

Goal state after:
n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
key : ↑n = ∑ i ∈ range n, (1 - ζ ^ i)
i : ℕ
x✝ : i ∈ range n
h : ζ - 1 ∣ 1 - ζ ^ i
⊢ ζ - 1 ∣ 1 - ζ ^ i
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 : (Quotient.mk I) ↑ζ = 1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := ↑↑ζ
hμ : IsPrimitiveRoot μ t
⊢ (absNorm I).Coprime t

Tactic:
exact Nat.dvd_one.mp (hI₂ ▸ Nat.gcd_dvd_gcd_of_dvd_right (absNorm I) ht)

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

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

Tactic:
exact interior_maximal (Set.image_mono interior_subset) this

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
h✝ : w = w₀
⊢ IsCompact {0}

Tactic:
exact isCompact_singleton

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ (fun w ↦ if w = w₀ then Real.log c else y w) ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1

Tactic:
Set.mem_univ_pi

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ ∀ (i : InfinitePlace K), (if i = w₀ then Real.log c else y i) ∈ if i = w₀ then Set.Iic 0 else Set.Icc 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : ¬x = 0
⊢ x ∈ compactSet K ↔ x ∈ ↑expMapBasis '' closure (paramSet K) ∪ {0}

Tactic:
refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : ¬x = 0
hx : x ∈ ↑expMapBasis '' closure (paramSet K) ∪ {0}
⊢ x ∈ compactSet K
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
obtain ⟨p, hp1, hp2⟩ := NumberField.exists_not_isUnramifiedIn (𝒪 := 𝒪) H
  have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
  have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
  have := IsIntegralClosure.isTorsionFree ℤ (A := 𝒪) K
  have := IsIntegralClosure.isIntegral_algebra ℤ (A := 𝒪) K
  grind [Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain]

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

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁶ : IsDomain 𝒪
this✝⁵ : IsDedekindDomain 𝒪
this✝⁴ : IsFractionRing 𝒪 K
this✝³ : Module.Finite ℤ 𝒪
this✝² : CharZero 𝒪
this✝¹ : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this✝ : IsGaloisGroup Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w✝ : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Ideal.under ℤ P = Ideal.span {p}
hp0 : p ≠ 0
this : Prime p
Q : Ideal 𝒪
x✝ : Q.IsPrime
hQ : ↑p.natAbs ∈ Q
⊢ (algebraMap ℤ 𝒪) ↑p.natAbs ∈ Q

Tactic:
by simpa using hQ

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
rw [posPart_eq_self.2 hsign]

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * A i j