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

Goal state before:
pp: k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)

Tactic:
have : d ≠ 0 := ofReal_ne_zero.mpr <| abs_ne_zero.mpr <| NeZero.ne _

Goal state after:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: case mp
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ Γ, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
⊢ γ ∈ s → f ∣[k] γ = f

Tactic:
hγ

Goal state after:
case mp
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ Γ, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ s
⊢ f ∣[k] γ = f
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: case mpr
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
⊢ γ ∈ Γ → f ∣[k] γ = f

Tactic:
hγ

Goal state after:
case mpr
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ f ∣[k] γ = f
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case zero
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ ⇑(f.pow 0) = ⇑f ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ ⟨0 • k, GradedMonoid.GMonoid.gnpow 0 f⟩ = ⟨↑0 * k, f.pow 0⟩

Tactic:
| zero =>

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

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst✝³ : ModularFormClass F Γ k
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : DiscreteTopology ↥Γ
inst✝ : Fact (IsCusp OnePoint.infty Γ)
⊢ ∃ c > 0, (fun τ ↦ f τ - valueAtInfty ⇑f) =O[atImInfty] fun τ ↦ rexp (-c * τ.im)

Tactic:
by
  have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
  have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
  refine ⟨2 * π / Γ.strictWidthInfty, div_pos Real.two_pi_pos hh, ?_⟩
  convert! exp_decay_sub_atImInfty hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f) using
    3 with τ
  ring_nf

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'
this : 3 * c ^ 2 ≤ 4
⊢ |↑g 1 0| ≤ 1

Tactic:
by
    rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_le] at this
    replace this : c' ^ 2 ≤ 1 ^ 2 := by lia
    rwa [sq_le_sq, abs_one] at this

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

Goal state before:
pp: case inl
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ DifferentiableOn ℂ (fun z ↦ (↑(a 0) * z + ↑(a 1)) ^ (-k)) {z | 0 < z.im}

Tactic:
apply DifferentiableOn.zpow

Goal state after:
case inl.hf
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ DifferentiableOn ℂ (fun x ↦ ↑(a 0) * x + ↑(a 1)) {z | 0 < z.im}

case h
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ (∀ x ∈ {z | 0 < z.im}, ↑(a 0) * x + ↑(a 1) ≠ 0) ∨ 0 ≤ -k
Module: Mathlib.NumberTheory.ModularForms.QExpansion

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

Tactic:
| zero =>

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

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
h2 : HasFPowerSeriesAt (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0
⊢ HasFPowerSeriesOnBall (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1

Tactic:
simpa [h1.eq_formalMultilinearSeries h2] using hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf

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

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ atTop ≤ Filter.comap (fun N ↦ Ico (-N) N) atTop

Tactic:
← @tendsto_iff_comap

Goal state after:
G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ Tendsto (fun N ↦ Ico (-N) N) atTop atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ atTop ≤ Filter.comap (fun N ↦ Ioc (-N) N) atTop

Tactic:
← @tendsto_iff_comap

Goal state after:
G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ Tendsto (fun N ↦ Ioc (-N) N) atTop atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ atTop ≤ Filter.comap (fun g ↦ Ioo (-g) g) atTop

Tactic:
← @tendsto_iff_comap

Goal state after:
G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ Tendsto (fun g ↦ Ioo (-g) g) atTop atTop
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left✝ : sSup ((fun q ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
⊢ ‖?m.238‖ < 1

Tactic:
by simpa [Metric.mem_ball, dist_zero_right] using hK hq₀

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

Goal state before:
pp: ⊢ MultipliableLocallyUniformlyOn (fun n q ↦ 1 - q ^ (n + 1)) (Metric.ball 0 1)

Tactic:
use fun q ↦ ∏' n, (1 - q ^ (n + 1))
  simp_rw [sub_eq_add_neg]
  apply hasProdLocallyUniformlyOn_of_forall_compact Metric.isOpen_ball
  intro K hK hcK
  rcases K.eq_empty_or_nonempty with hN | hN
  · simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn, hN] using tendstoUniformlyOn_empty
  · obtain ⟨q₀, hq₀, _, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN
      (show ContinuousOn (fun q : ℂ ↦ ‖q‖) K by fun_prop)
    refine ((summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _)
      (by simpa [Metric.mem_ball, dist_zero_right] using hK hq₀))).hasProdUniformlyOn_nat_one_add
      hcK (.of_forall fun n x hx ↦ ?_) (fun _ ↦ by fun_prop)
    simpa using pow_le_pow_left₀ (norm_nonneg _) (HB x hx) (n + 1)

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

Goal state before:
pp: x✝ : Finset ℕ
⊢ DifferentiableOn ℂ (fun x2 ↦ ∏ i ∈ x✝, (fun n q ↦ 1 - q ^ (n + 1)) i x2) (Metric.ball 0 1)

Tactic:
by simpa [Finset.prod_fn] using
      DifferentiableOn.finsetProd (fun _ _ ↦ by fun_prop)

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
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
⊢ T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T

Tactic:
hgeq,

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

Goal state before:
pp: z : ℍ
⊢ ∑' (m : Fin 2 → ℤ), G2Term z m = ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]

Tactic:
rw [← (finTwoArrowEquiv _).symm.tsum_eq]

Goal state after:
z : ℍ
⊢ ∑' (c : ℤ × ℤ), G2Term z ((finTwoArrowEquiv ℤ).symm c) = ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
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)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹

Tactic:
hgeq,

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

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv ((F + G) ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z + (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z

Tactic:
show (F + G) ∘ ofComplex = F ∘ ofComplex + G ∘ ofComplex from rfl,

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex + G ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z + (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ (Δ ∣[12] ModularGroup.S) z = Δ z

Tactic:
suffices η (-(↑z)⁻¹) ^ 24 * ((z : ℂ) ^ 12)⁻¹ = η z ^ 24 by
    rw [SL_slash_apply, UpperHalfPlane.modular_S_smul]
    simpa [denom, ModularGroup.S]

Goal state after:
z : ℍ
⊢ η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
Module: Mathlib.NumberTheory.Modular

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

Tactic:
grind [case_c_one_d_neg_one hz hg him.le hc hd]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ IsClosed fun z ↦ Real.le✝ |z.re| (1 / 2)

Tactic:
exact isClosed_le (f := fun z : ℍ ↦ |z.re|) (by fun_prop) continuous_const

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
a : ℝ
ha : 0 < a
ha' : a ∈ Set.Iio 1
this : a * |x.re| < 1 / 2
⊢ |(↑{ coe := ↑a * ↑x, coe_im_pos := ⋯ }).re| < 1 / 2

Tactic:
by simpa [abs_of_pos ha]

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✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 0)

Tactic:
rw [show (0 : ℂ) = ∑ c : ℋ ⧸ 𝒢.subgroupOf ℋ, 0 by simp]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 (∑ c, 0))
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case refine_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
⊢ HasSum
    (fun i ↦
      if 2 * ↑i / h Γ = 0 then 0 else (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑i / h Γ) * t)))
    ((weakFEPair hk f).f t - (weakFEPair hk f).f₀)

Tactic:
convert! hasSum_ite_sub_hasSum this 0 using 2 with n

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
n : ℕ
⊢ (if 2 * ↑n / h Γ = 0 then 0 else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑n / h Γ) * t))) =
    if n = 0 then 0
    else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ n

case e'_6.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
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
⊢ (weakFEPair hk f).f₀ =
    (PowerSeries.coeff 0) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ 0
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x ^ 2 ^ 0 - y ^ 2 ^ 0 = (∏ i ∈ range 0, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
| zero =>

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)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst✝¹ : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst✝¹ i] (A' i)
X : Type u_4
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
⊢ Continuous[instTopologicalSpaceProd, inst✝] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))

Tactic:
simp_rw [continuous_dom_prod_right hAopen, continuous_dom_prod_left hAopen']

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst✝¹ : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst✝¹ i] (A' i)
X : Type u_4
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
⊢ (∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S) (S_1 : Set ι) (hS_1 : cofinite ≤ 𝓟 S_1),
      Continuous[instTopologicalSpaceProd, inst✝]
        ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hS_1))) ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ normAtComplexPlaces a ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0

Tactic:
refine ⟨?_, by simpa using h a⟩

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ normAtComplexPlaces a ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑x ∈ K⁺
⊢ ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x

Tactic:
have : IsIntegral ℤ (⟨x, h⟩ : K⁺) :=
      (isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K⁺ K)).mp x.isIntegral_coe

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑x ∈ K⁺
this : IsIntegral ℤ ⟨↑x, h⟩
⊢ ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : (ringOfIntegersComplexConj K) x = x
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))

pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) → (ringOfIntegersComplexConj K) x = x

Tactic:
· rw [RingOfIntegers.ext_iff, coe_ringOfIntegersComplexConj,
      RingOfIntegers.complexConj_eq_self_iff] at h
    obtain ⟨y, hy⟩ := h
    exact ⟨y, RingOfIntegers.ext_iff.mpr hy⟩

Goal state after:
case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) → (ringOfIntegersComplexConj K) x = x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case zero
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∑ w, 0 w = 0

Tactic:
| zero =>

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ (if hi : ↑i = w₀ then fun w ↦ ↑w.mult
    else
      ↑expMap.symm
        (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, hi⟩)))))) =
    ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))))

Tactic:
dif_neg

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ ↑expMap.symm
      (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, ?hnc⟩))))) =
    ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))))

case hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ ¬↑i = w₀
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' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * |((reindex g g) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e i)))))).det| =
    ↑(finrank ℚ K) *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|

Tactic:
congr with i j

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ (reindex g g) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e i))))) i j =
    (of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
      (fun x ↦ f ((f.symm w').succAbove x)) (fun x ↦ f ((f.symm w').succAbove x)) i j