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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : Γ.HasDetPlusMinusOne
k₁ k₂ : ℤ
f : SlashInvariantForm Γ k₁
g : SlashInvariantForm Γ k₂
A : GL (Fin 2) ℝ
hA : A ∈ Γ
⊢ (⇑f * ⇑g) ∣[k₁ + k₂] A = ⇑f * ⇑g

Tactic:
simp [mul_slash, Subgroup.HasDetPlusMinusOne.abs_det hA,
    -Matrix.GeneralLinearGroup.val_det_apply, slash_action_eqn f A hA, slash_action_eqn g A hA]

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
this : DiscreteTopology ↥(map (mapGL ℝ) Γ).strictPeriods
⊢ (map (mapGL ℝ) Γ).strictWidthInfty = 1

Tactic:
rw [strictPeriods_eq_zmultiples_strictWidthInfty, Eq.comm,
    AddSubgroup.zmultiples_eq_zmultiples_iff (not_isOfFinAddOrder_of_isAddTorsionFree one_ne_zero)]
    at hsp

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : 1 = (map (mapGL ℝ) Γ).strictWidthInfty ∨ -1 = (map (mapGL ℝ) Γ).strictWidthInfty
this : DiscreteTopology ↥(map (mapGL ℝ) Γ).strictPeriods
⊢ (map (mapGL ℝ) Γ).strictWidthInfty = 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (f c).im = c 0

Tactic:
f_def,

Goal state after:
case «0»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * ((fun p ↦ ↑(p 0) * ↑z + ↑(p 1)) c).im = c 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * (starRingEnd ℂ) (f c)).im = c 1

Tactic:
f_def,

Goal state after:
case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * (starRingEnd ℂ) ((fun p ↦ ↑(p 0) * ↑z + ↑(p 1)) c)).im = c 1
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetPlusMinusOne
k₁ k₂ : ℤ
f : CuspForm Γ k₁
g : ModularForm Γ k₂
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
⊢ IsZeroAtImInfty ((f.mul g.toSlashInvariantForm).toFun ∣[k₁ + k₂] γ)

Tactic:
by
    simpa [mul_slash] using!
      ((f.zero_at_cusps' hc γ hγ).mul_boundedAtFilter (g.bdd_at_cusps' hc γ hγ)).smul _

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

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2 + k) * (starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
      (↑τ.im ^ k * ↑(Complex.normSq j) ^ (-k)) =
    ↑D ^ (k - 2) *
      ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * ((↑D * ↑τ.im) ^ k / ↑(Complex.normSq j) ^ k))

Tactic:
mul_zpow,

Goal state after:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2 + k) * (starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
      (↑τ.im ^ k * ↑(Complex.normSq j) ^ (-k)) =
    ↑D ^ (k - 2) *
      ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D ^ k * ↑τ.im ^ k / ↑(Complex.normSq j) ^ k))
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

Tactic:
by
  -- previous lemma gives result after updating at 0
  have H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (.ofScalars ℂ c) 0 1 :=
    hasFPowerSeriesOnBall_update hh hf
  -- now just need to check values at 0 match
  -- use continuity of both functions & we know it everywhere else
  have H2 : c 0 = cuspFunction h f 0 := by
    have L1 := H1.hasFPowerSeriesAt.continuousAt
    have L2 := hfanalytic.continuousAt
    have := (L1.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE L2).mp <|
      by filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..
    simpa [update_self] using this.eq_of_nhds
  rwa [update_eq_self_iff.mpr H2] at H1

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

Goal state before:
pp: k : ℤ
hk : 0 ≤ 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✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
conv => enter [1, C, τ, 1]; rw [← norm_norm]

Goal state after:
k : ℤ
hk : 0 ≤ 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✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖‖petersson k (⇑f) (⇑f') τ‖‖ ≤ C * max τ.im (1 / τ.im) ^ k
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 => enter [1, C, τ, 1]; rw [← norm_norm]

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') τ‖‖ ≤ C
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
⊢ (g = S * T ∨ g = T * S * T) ∧ z = ρ

Tactic:
rw [hgeq]

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
⊢ (T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T) ∧ z = ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹

Tactic:
rw [hgeq]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
⊢ T ^ ↑g 0 0 * S * T⁻¹ = S * T⁻¹ ∨ T ^ ↑g 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ (I ^ 4) ^ 3 = 1

Tactic:
I_pow_four,

Goal state after:
⊢ 1 ^ 3 = 1
Module: Mathlib.NumberTheory.Modular

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

Tactic:
intro ξ hξ

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

Goal state before:
pp: ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 𝒟 ⊆ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)

Tactic:
intro ξ hξ

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
ξ : ℍ
hξ : ξ ∈ 𝒟
⊢ ξ ∈ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ 𝒟ᵒ = interior 𝒟

Tactic:
refine subset_antisymm (isOpen_fdo.subset_interior_iff.mpr fdo_subset_fd) ?_
  have ho1 := isOpenMap_re.image_interior_subset 𝒟
  have ho2 := isOpenMap_norm.image_interior_subset 𝒟
  intro x hx
  rw [Set.image_subset_iff] at *
  constructor
  · rw [one_lt_normSq_iff, ← Set.mem_Ioi, ← interior_Ici]
    apply Set.mem_of_mem_of_subset (Set.mem_preimage.mp (ho2 hx)) (interior_mono ?_)
    rw [Set.image_subset_iff]
    intro ξ hξ
    simpa [Set.mem_preimage, Set.mem_Ici, one_le_normSq_iff] using hξ.1
  · rw [abs_lt, ← Set.mem_Ioo, ← interior_Icc]
    apply Set.mem_of_mem_of_subset ((Set.mem_preimage.mp (ho1 hx))) (interior_mono ?_)
    rw [Set.image_subset_iff]
    intro ξ hξ
    simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : SlashInvariantFormClass F 𝒢 k
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ℋ.HasDetPlusMinusOne
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (let this := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
      ∏ q, quotientFunc f q) ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))]
      h =
    let this := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
    ∏ q, quotientFunc f q

Tactic:
simpa [← Finset.card_univ, ModularForm.prod_slash,
      quotientFunc_smul f hh, Subgroup.HasDetPlusMinusOne.abs_det hh,
      -Matrix.GeneralLinearGroup.val_det_apply] using Equiv.prod_comp (MulAction.toPerm (_ : ℋ)) _

Goal state after:
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
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (∏ i, quotientFunc f i ∣[k] γ) =O[atImInfty] fun x ↦ ∏ i, 1

Tactic:
Finset.prod_fn

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
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (fun a ↦ ∏ c, (quotientFunc f c ∣[k] γ) a) =O[atImInfty] fun x ↦ ∏ i, 1
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e_6
Γ : 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
⊢ ↑{ coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
        { coe := I * ↑t, coe_im_pos := ⋯ })

Tactic:
coe_smul_of_det_pos (by simp)

Goal state after:
case e_6
Γ : 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
⊢ ↑{ coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    num (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ } /
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ }
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:

Tactic:
ProperlyDiscontinuousSMul G α ↔ ProperlyDiscontinuousSMul ↑(G ⊓ H) α :=
    (properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_left).symm
  _ ↔ ProperlyDiscontinuousSMul H α :=
    properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_right

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
⊢ (Support R k).Finite

Tactic:
by
    apply Set.Finite.subset this
    intro v hv
    apply_fun v.valuation K at hk
    simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
    rw [Set.mem_ofPred_eq, valuation_of_algebraMap]
    have := intValuation_le_one v n
    contrapose! this
    rw [← hk, mul_comm]
    exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
      mul_le_mul_of_nonneg_right this (by simp)

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)
X : Type u_3
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i]_[𝓕] → X
⊢ Continuous[topologicalSpace R A 𝓕, inst✝] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), Continuous[topologicalSpace R A (𝓟 S), inst✝] (f ∘ inclusion R A hS)

Tactic:
by
  simp_rw +instances [topologicalSpace_eq_of_principal, continuous_iSup_dom,
    continuous_coinduced_dom]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : Odd x
hn : Even n
⊢ Odd y

Tactic:
replace hxy := (@even_neg _ _ (x - y)).mpr (even_iff_two_dvd.mpr hxy)

Goal state after:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ Odd y
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)

Tactic:
have : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3 := by
    refine (padicValNat_dvd_iff_le (by grind [mul_ne_zero])).mp ?_
    simp [← Nat.pow_two_sub_pow_two x 1]
    grind [Nat.eight_dvd_sq_sub_one_of_odd]

Goal state after:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
this : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ ∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      ∫⁻ (y : { w // w.IsComplex } → ℝ) in Set.univ.pi fun x ↦ Set.Ioo (-π) π,
        (∏ w, ENNReal.ofReal ((x, y).1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm (x, y)) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
simp_rw [hA', normAtComplexPlaces_polarSpaceCoord_symm, lintegral_const, restrict_apply
      MeasurableSet.univ, Set.univ_inter, volume_pi, Measure.pi_pi, volume_Ioo, sub_neg_eq_add,
      ← two_mul, Finset.prod_const, Finset.card_univ, ← Set.indicator_const_mul,
      ← Set.indicator_comp_right, Function.comp_def, Pi.one_apply, mul_one]
    rw [lintegral_mul_const' _ _ (ne_of_beq_false rfl).symm, mul_comm]
    erw [setLIntegral_indicator (by convert! hm.preimage mixedSpaceOfRealSpace.measurable)]
    rw [hA, volume_eq_two_pi_pow_mul_integral_aux hA]
    congr 1
    refine setLIntegral_congr (ae_eq_set_inter (by rfl) (Measure.ae_eq_set_pi fun w _ ↦ ?_))
    split_ifs
    exacts [ae_eq_rfl, Ioi_ae_eq_Ici]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ ∃ u, u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ integerSet K

Tactic:
exact ⟨u, mem_integerSet.mpr ⟨hu, u * x, by simp_rw [unitSMul_smul, ← map_mul]⟩⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMap x)) = 1
x✝ : { w // w ≠ w₀ }
⊢ logMap (mixedSpaceOfRealSpace (↑expMap x)) x✝ = x ↑x✝

Tactic:
rw [logMap, normAtPlace_mixedSpaceOfRealSpace (Real.exp_nonneg _), expMap_apply, Real.log_exp,
    mul_sub, mul_inv_cancel_left₀ mult_coe_ne_zero, hx, Real.log_one, zero_mul, mul_zero, sub_zero]

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

Goal state before:
pp: case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ ∑ x,
      ↑expMap.symm
        (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑w, ⋯⟩))))) x =
    0

Tactic:
sum_expMap_symm_apply (coe_ne_zero _),

Goal state after:
case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ Real.log ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑w, ⋯⟩)))| = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ ↑expMap ((completeBasis K) ↑i) =
    normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))))

Tactic:
completeBasis_apply_of_ne,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ ↑expMap
      (↑expMap.symm
        (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))))) =
    normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1,
          x ↑x_1 •
            (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦ (completeBasis K) ↑x_1 ↑i)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
completeBasis_apply_of_ne,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1,
          x ↑x_1 •
            (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
              ↑expMap.symm
                (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1)))))
                ↑i)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
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)

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < ↑(torsionOrder K) * √|↑(discr K)|

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

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < ↑(torsionOrder K) * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: 𝒪 : Type u_2
inst✝⁴ : CommRing 𝒪
inst✝³ : Module.Finite ℤ 𝒪
inst✝² : Algebra.Unramified ℤ 𝒪
inst✝¹ : IsDomain 𝒪
inst✝ : FaithfulSMul ℤ 𝒪
this✝³ : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this✝² : Algebra ℤ K := Ring.toIntAlgebra K
this✝¹ : CharZero 𝒪
this✝ : NumberField K
this : Module.finrank ℚ K = 1
⊢ Function.Bijective ⇑(algebraMap ℤ 𝒪)

Tactic:
have : IsIntegralClosure ℤ ℤ K := .of_algEquiv _ (.ofBijective (IsScalarTower.toAlgHom _ _ _)
    (Algebra.finrank_eq_one_iff_bijective_algebraMap.mp this)) (by simp)

Goal state after:
𝒪 : Type u_2
inst✝⁴ : CommRing 𝒪
inst✝³ : Module.Finite ℤ 𝒪
inst✝² : Algebra.Unramified ℤ 𝒪
inst✝¹ : IsDomain 𝒪
inst✝ : FaithfulSMul ℤ 𝒪
this✝⁴ : IsDedekindDomain 𝒪
K : Type u_2 := FractionRing 𝒪
this✝³ : Algebra ℤ K := Ring.toIntAlgebra K
this✝² : CharZero 𝒪
this✝¹ : NumberField K
this✝ : Module.finrank ℚ K = 1
this : IsIntegralClosure ℤ ℤ K
⊢ Function.Bijective ⇑(algebraMap ℤ 𝒪)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case hd
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := ⋯
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⋯
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ 0 < -Real.log (max (f ↑p) (f ↑m))

Tactic:
simp only [Left.neg_pos_iff]

Goal state after:
case hd
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ Real.log (max (f ↑p) (f ↑m)) < 0