mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)

Tactic:
induction n with

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Finite 𝓀[K]

Tactic:
rw [← Set.finite_univ_iff]

Goal state after:
case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Set.univ.Finite
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
this✝² : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this✝¹ : IsUniformAddGroup K
val✝ : LocallyFiniteOrder (↥(MonoidHom.mrange Valued.v))ˣ
e : ↥(MonoidHom.mrange (valuation K)) ≃*o ValueGroupWithZero K :=
  { toMulEquiv := MulEquiv.ofBijective (MonoidHom.mrange (valuation K)).subtype ⋯, map_le_map_iff' := ⋯ }
this✝ : Nontrivial (ValueGroupWithZero K)ˣ
this : Nontrivial (↥(MonoidHom.mrange (valuation K)))ˣ
⊢ Nonempty (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))

Tactic:
exact ⟨e.symm.trans (LocallyFiniteOrder.orderMonoidWithZeroEquiv _)⟩

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
⊢ 2 ^ (n + 1) - 1 = 2 * (2 ^ n - 1) + 1

Tactic:
have := Nat.one_le_pow n 2 two_pos

Goal state after:
n : ℕ
this : 1 ≤ 2 ^ n
⊢ 2 ^ (n + 1) - 1 = 2 * (2 ^ n - 1) + 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ sZMod (p' + 2) (i + 1) = ↑(s (i + 1))

Tactic:
push_cast [s, sZMod, ih]

Goal state after:
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
⊢ {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite ∧
    {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤ ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

Tactic:
rw [← h_card]

Goal state after:
n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
⊢ {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite ∧
    {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤
      {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
⊢ 𝒢.adjoinNegOne.HasDetPlusMinusOne ↔ 𝒢.HasDetPlusMinusOne

Tactic:
by
  refine ⟨fun _ ↦ ⟨fun {g} hg ↦ HasDetPlusMinusOne.det_eq (𝒢.le_adjoinNegOne hg)⟩, fun _ ↦ ⟨?_⟩⟩
  rintro g (hg | hg)
  · exact HasDetPlusMinusOne.det_eq hg
  · by_cases hn : Even (Fintype.card n)
    · convert! HasDetPlusMinusOne.det_eq hg using 1 <;>
        simp [Units.ext_iff, det_neg, hn]
    · convert! (HasDetPlusMinusOne.det_eq hg).symm using 1 <;>
        simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    (↑A₂.den)⁻¹ • (a₁ * a₂ * M) • (↑A₁.den)⁻¹ • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)

Tactic:
← Nat.cast_smul_eq_nsmul ℚ (_ * M),

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    (↑A₂.den)⁻¹ • ↑(a₁ * a₂ * M) • (↑A₁.den)⁻¹ • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
⊢ g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
induction n with

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

Goal state before:
pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0

Tactic:
simpa [Subgroup.inf_relIndex_right] using h𝒢.1

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
x : R
⊢ x ∈ 𝒢.strictPeriods ↔ upperRightHom x ∈ 𝒢

Tactic:
by
  simp [strictPeriods]

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

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : g • ∞ = ∞
⊢ AddSubgroup.zmultiples 𝒢.strictWidthInfty ≠ ⊥

Tactic:
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]

Goal state after:
case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : g • ∞ = ∞
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N) →
    ∃ x_1, (↑(↑x_1 0 0) = 1 ∧ ↑(↑x_1 0 1) = 0 ∧ ↑(↑x_1 1 0) = 0 ∧ ↑(↑x_1 1 1) = 1) ∧ (mapGL ℝ) x_1 = upperRightHom x

Tactic:
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.Basic

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

Tactic:
induction n with

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

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

Tactic:
induction n with

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

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖qExpansionFormalMultilinearSeries h f m‖ = ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖

Tactic:
by
  rw [qExpansionFormalMultilinearSeries,
    ← (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm.norm_map]
  simp

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) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D * ↑τ.im / ↑(Complex.normSq j)) ^ k) =
    ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * ↑(g • τ).im ^ k)

Tactic:
by
    rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]

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

Goal state before:
pp: case hasSum.inl
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hy : ‖0‖ < 1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ 0) (update (cuspFunction h f) 0 (c 0) (0 + 0))

Tactic:
simpa +contextual [zero_pow_eq] using hasSum_ite_eq 0 (c 0)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ (T⁻¹ • z).im = z.im

Tactic:
simpa using im_T_zpow_smul z (-1)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : ℍ → SL(2, ℤ) ⧸ Γ → E := fun τ ↦ Quotient.lift (fun g ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty : ∀ (γ : SL(2, ℤ) ⧸ Γ), (fun x ↦ f' x γ) =O[atImInfty] fun z ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
obtain ⟨C, hC⟩ := exists_bound_of_invariant_of_isBigO (by fun_prop) ht
    (.fun_sum fun i _ ↦ (hf'_infty i).norm_left)
    (fun g τ ↦ (Fintype.sum_equiv (MulAction.toPerm g) _ _ (by simp [-sl_moeb, hf'_inv])).symm)

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : ℍ → SL(2, ℤ) ⧸ Γ → E := fun τ ↦ Quotient.lift (fun g ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty : ∀ (γ : SL(2, ℤ) ⧸ Γ), (fun x ↦ f' x γ) =O[atImInfty] fun z ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), ‖∑ c, ‖f' τ c‖‖ ≤ C * max τ.im (1 / τ.im) ^ t
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
let R := Real.exp (-2 * π * t / h)
  have hR0 : 0 < R := Real.exp_pos _
  have hR1 : R < 1 := Real.exp_lt_one_iff.2 <| by simpa [neg_div] using div_pos (by positivity) hh
  -- First apply `qExpansion_coeff_eq_circleIntegral` and rescale from `0 .. 2 * π` to `0 .. h`.
  rw [qExpansion_coeff_eq_circleIntegral hh hfper hfhol hfbdd n hR0 hR1, circleIntegral,
    show 2 * π = h * (2 * π / h) by field_simp]
  conv => enter [1, 2, 2]; rw [show 0 = 0 * (2 * π / h) by simp]
  simp_rw [← intervalIntegral.smul_integral_comp_mul_right, real_smul, ← mul_assoc,
    ← intervalIntegral.integral_const_mul]
  -- Compare the integrands
  congr 1 with u
  let τ : ℍ := ⟨u + t * I, by simpa using ht⟩
  have : circleMap 0 R (u * (2 * π / h)) = 𝕢 h τ := by
    simp only [circleMap, ofReal_exp, ← exp_add, zero_add, τ, R]
    congr 1
    push_cast
    have := I_sq
    grind
  -- now just complex exponential arithmetic to finish
  simp_rw [deriv_circleMap, this, show ↑I = Complex.I by rfl, show u + t * Complex.I = τ by rfl,
    show ⟨↑τ, τ.2⟩ = τ by rfl, eq_cuspFunction _ hh.ne' hfper, smul_eq_mul, pow_succ]
  field_simp [(show 𝕢 h τ ≠ 0 from Complex.exp_ne_zero _), Real.pi_ne_zero, NeZero.ne]
  push_cast
  ring

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'
⊢ 3 * c ^ 2 ≤ 4

Tactic:
suffices c ≠ 0 → 9 * c ^ 4 ≤ 16 by
    rcases eq_or_ne c 0 with (hc | hc)
    · simp [hc]
    · apply le_of_sq_le_sq <;> grind

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ c ≠ 0 → 9 * c ^ 4 ≤ 16
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case inr
h : ℝ
m : ℕ
q : ℂ
hq : q ≠ 0
⊢ cuspFunction h 1 q = 1 q

Tactic:
simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero h _ hq]

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

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

Tactic:
induction n with

Goal state after:
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 ^ k / ‖↑(t ^ k)‖₊) ((1 / t) ^ k / ‖↑(t ^ k)‖₊) = max (1 ^ 2) ((1 / t ^ k) ^ 2)

Tactic:
congr <;> simp [field, ht.ne']

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ↑n ^ k * r ^ n / (1 - r ^ n)

Tactic:
by
  simp only [div_eq_mul_one_div (_ * _ ^ _)]
  apply Summable.mul_tendsto_const (c := 1 / (1 - 0))
    (by simpa using! summable_norm_pow_mul_geometric_of_norm_lt_one k hr)
  simpa only [Nat.cofinite_eq_atTop] using!
   tendsto_const_nhds.div ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).const_sub 1) (by simp)

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 : ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ k * r ^ (↑d * ↑c) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
⊢ Summable (Function.uncurry fun c d ↦ ↑↑c ^ k * r ^ (↑d * ↑c))

Tactic:
by apply (summable_prod_mul_pow k hr).prod_symm

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

Goal state before:
pp: z : ℂ
⊢ ∑' (n : ℕ), logDeriv (fun x ↦ 1 - eta_q n x) z = 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n z / (1 - eta_q n z)

Tactic:
by
  rw [tsum_congr (one_sub_eta_logDeriv_eq z), ← tsum_mul_left]
  grind

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

Goal state before:
pp: z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 *
      ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
        (2 * (↑π ^ 2 / 6) - 8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n))

Tactic:
← tsum_pow_div_one_sub_eq_tsum_sigma
    (norm_exp_two_pi_I_lt_one z),

Goal state after:
z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 *
      ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
        (2 * (↑π ^ 2 / 6) -
          8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ↑n / (1 - cexp (2 * ↑π * I * ↑z) ^ ↑n)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
h :
  -(2 * ↑π * I * (2 * ↑π * I) ^ k) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n =
    -(2 * ↑π * I) * ∑' (n : ℕ), (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n
⊢ (fun n ↦ iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z) = fun n ↦
    (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
ext n

Goal state after:
case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
h :
  -(2 * ↑π * I * (2 * ↑π * I) ^ k) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n =
    -(2 * ↑π * I) * ∑' (n : ℕ), (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z = (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
⊢ (fun x ↦ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑x ^ k * cexp (2 * ↑π * I * ↑z) ^ x))) = fun x ↦
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑x ^ k * cexp (2 * ↑π * I * ↑z) ^ x)

Tactic:
ext n

Goal state after:
case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)) =
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case 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
⊢ (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:
· rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz him.le hc) with hd | hd | hd
    · grind [cases_c_one_d_zero hz hg him.le hc hd] -- ± S, T⁻¹S, TS
    · grind [case_c_one_d_one hz hg him.le hc hd] -- ± ST, TST
    · grind [case_c_one_d_neg_one hz hg him.le hc hd]

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

Goal state before:
pp: z : ℍ
N : ℕ
n : ℤ
hn : n ∈ Ico (-↑N) ↑N
⊢ (↑z ^ 2)⁻¹ * ∑' (n_1 : ℤ), ((-(↑n * (↑z)⁻¹) + ↑n_1) ^ 2)⁻¹ = ∑' (b : ℤ), ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
rw [← tsum_mul_left, ← tsum_comp_neg]

Goal state after:
z : ℍ
N : ℕ
n : ℤ
hn : n ∈ Ico (-↑N) ↑N
⊢ ∑' (d : ℤ), (↑z ^ 2)⁻¹ * ((-(↑n * (↑z)⁻¹) + ↑(-d)) ^ 2)⁻¹ = ∑' (b : ℤ), ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
rw [← (finTwoArrowEquiv ℤ).symm.tsum_eq, finTwoArrowEquiv_symm_apply,
    Summable.tsum_prod (summable_prod_eisSummand hk z),
    tsum_int_eq_zero_add_two_mul_tsum_pnat (fun n ↦ ?h₁)
      (by simpa using (summable_prod_eisSummand hk z).prod)]
  case h₁ =>
    nth_rewrite 1 [← tsum_comp_neg]
    exact tsum_congr fun y ↦ by simp [eisSummand, ← neg_add _ (y : ℂ), -neg_add_rev, hk2.neg_pow]
  have H (b : ℕ+) := qExpansion_identity_pnat (k := k - 1) (by grind) ⟨b * z, by simpa using z.2⟩
  simp_rw [show k - 1 + 1 = k by grind, one_div] at H
  simp only [neg_mul] at H
  rw [nsmul_eq_mul, mul_assoc]
  congr
  · simp [eisSummand, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even (by grind) hk2]
  · suffices ∑' (m : ℕ+) (n : ℕ+), (n : ℕ) ^ (k - 1) * cexp (2 * π * I * (m * z)) ^ (n : ℕ) =
        ∑' (m : ℕ+) (n : ℕ+), (n : ℕ) ^ (k - 1) * cexp (2 * π * I * z) ^ (m * n : ℕ) by
      simp [eisSummand, H, tsum_mul_left,
        ← tsum_prod_pow_eq_tsum_sigma (k - 1) (norm_exp_two_pi_I_lt_one z), this]
    simp_rw [← Complex.exp_nat_mul]
    exact tsum_congr₂ (fun m n ↦ by push_cast; ring_nf)

Goal state after:
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
S : Subgroup Γ
⊢ ProperlyDiscontinuousSMul (↥S) α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
properlyDiscontinuousSMul_iff

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
S : Subgroup Γ
⊢ (∀ {K L : Set α}, IsCompact K → IsCompact L → {m | (m • K ∩ L).Nonempty}.Finite) ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite
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:
| hp =>

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange

Tactic:
contrapose hv

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
⊢ ¬v.IsComplex
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: 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
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
⊢ (fun i ↦ (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) / ↑i ^ s) = fun i ↦
    ↑π ^ (-s) * Gamma s * (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑i / h Γ) ^ s *
      (2 / s.Gammaℂ * ↑(h Γ) ^ (-s))

Tactic:
ext 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
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
⊢ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑n ^ s =
    ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s *
      (2 / s.Gammaℂ * ↑(h Γ) ^ (-s))