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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1

Tactic:
let t₀ := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ Tendsto (fun N ↦ termSum s N) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
simp_rw [termSum_of_lt _ hs]

Goal state after:
s : ℝ
hs : 1 < s
⊢ Tendsto
    (fun N ↦
      1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s))
    atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (x + -y) ≤ 2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ (-y)

Tactic:
exact mulHeight₁_add_le x (-y)

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.toList.length = ∑ i, 1

Tactic:
Fin.sum_const,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.toList.length = archAbsVal.toList.length • 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case hbc
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
j : ι'
⊢ ⨆ s, ↑v (coeff (↑s) (p j)) ≤ ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
· grw [← HH₂, ← le_max_left]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (InfinitePlace K)
n : ℕ
hn : n ≠ 0
v : InfinitePlace K
⊢ ↑n ^ (totalWeight K - 1) * ↑n = (∏ w ∈ univ.erase v, ↑n ^ w.mult) * ↑n ^ (v.mult - 1) * ↑n

Tactic:
rw [pow_sub_one_mul (totalWeight_pos K).ne', totalWeight_eq_sum_mult, ← prod_pow_eq_pow_sum,
    ← prod_erase_mul _ _ (mem_univ v), ← pow_sub_one_mul v.mult_ne_zero, ← mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
⊢ Function.Surjective ⇑(aeval α)

Tactic:
rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s✝ : ℂ
hs✝ : s✝ ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableWithinAt ℂ (fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) {1}ᶜ s

Tactic:
refine ((differentiableAt_LFunction _ _ (.inl hs)).mul ?_).differentiableWithinAt

Goal state after:
case refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s✝ : ℂ
hs✝ : s✝ ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ (fun s ↦ ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
n : ℕ
⊢ 0 ≤ χ.zetaMul n

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp only [ArithmeticFunction.map_zero, le_refl]
  · simpa only [χ.isMultiplicative_zetaMul.multiplicative_factorization _ hn] using!
      Finset.prod_nonneg
        fun p hp ↦ zetaMul_prime_pow_nonneg hχ (Nat.prime_of_mem_primeFactors hp) _

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case e'_5.e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))) = log (1 - ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y))))

Tactic:
congr 2
      rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, mul_left_comm]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ 2 * ((↑↑p)⁻¹ ^ (-1 / 2) * (↑↑p)⁻¹ ^ ↑(k + 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Tactic:
← Real.rpow_add <| by have := p.prop.pos; positivity,

Goal state after:
p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (-1 / 2 + ↑(k + 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
⊢ (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0 ↔ (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤

Tactic:
by
  by_cases h : abscissaOfAbsConv f = ⊤
  · simpa [h] using!
      Eventually.of_forall <| by simp [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h]
  · simp only [ne_eq, h, or_false]
    refine ⟨fun H ↦ ?_, fun H ↦ Eventually.of_forall fun x ↦ ?_⟩
    · let F (n : ℕ) : ℂ := if n = 0 then 0 else f n
      have hF₀ : F 0 = 0 := rfl
      have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
      suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)
      have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h
      have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr hF x
      have H' (n : ℕ) : (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) =ᶠ[atTop] fun _ ↦ 0 := by
        simp only [h']
        rw [eventuallyEq_iff_exists_mem] at H ⊢
        obtain ⟨s, hs⟩ := H
        exact ⟨s, hs.1, fun x hx ↦ by simp [hs.2 hx]⟩
      intro n
      induction n using Nat.strongRecOn with | ind n ih =>
      -- it suffices to show that `n ^ x * LSeries F x` tends to `F n` as `x` tends to `∞`
      suffices Tendsto (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) atTop (nhds (F n)) by
        replace this := this.congr' <| H' n
        simp only [tendsto_const_nhds_iff] at this
        exact this.symm
      cases n with
      | zero => exact Tendsto.congr' (H' 0).symm <| by simp [hF₀]
      | succ n =>
          simpa using! LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
            Ne.lt_top ha
    · simp [LSeries_congr (fun {n} ↦ H n) x, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
⊢ ∃ p > n, Prime p ∧ ↑p ≡ a [ZMOD ↑q]

Tactic:
have : NeZero q := ⟨hq⟩
  have : IsUnit (a : ZMod q) := by
    rwa [ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]
  obtain ⟨p, hpn, hpp, heq⟩ := forall_exists_prime_gt_and_eq_mod this n
  refine ⟨p, hpn, hpp, ?_⟩
  simpa [← ZMod.intCast_eq_intCast_iff] using heq

Goal state after:
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
n k : ℕ
hk : k ∈ Icc 1 n
⊢ (if k = 0 then 0 else f k) = f k

Tactic:
by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousConstVAdd R R
h₀ : ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {z | v z < ↑γ} ⊆ s
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, (fun x_1 ↦ x + x_1) '' {z | v z < ↑γ} ⊆ s

Tactic:
by
    simpa [← vadd_mem_nhds_vadd_iff (t := s) (-x), ← image_vadd, ← image_subset_iff] using
      h₀ ((x + ·) ⁻¹' s)

Goal state after:
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
have h₂ : IsBoundedUnder
      (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s : ℝ ↦ ‖(s - 1) * LSeries f s - s * l‖ := by
    obtain ⟨C, _, hC₂⟩ :=
      LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one
    exact h₁.isBoundedUnder_le.mono_le hC₂

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 1 < p
h : 1 ≤ sModNatTR (2 ^ p - 1) (p - 2)
⊢ ¬LucasLehmerTest p

Tactic:
Nat.succ_le_iff,

Goal state after:
p : ℕ
hp : 1 < p
h : 0 < sModNatTR (2 ^ p - 1) (p - 2)
⊢ ¬LucasLehmerTest p
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
this : Dense ↑H ∨ ∃ a, zpowers a = H
hA : DiscreteTopology ↥H
h : Dense ↑H
⊢ ↑H = _root_.closure ↑H

Tactic:
H.isClosed_of_discrete.closure_eq

Goal state after:
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
this : Dense ↑H ∨ ∃ a, zpowers a = H
hA : DiscreteTopology ↥H
h : Dense ↑H
⊢ ↑H = ↑H
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
⊢ ∀ {g : GL (Fin 2) ℝ}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1

Tactic:
intro g hg

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
⊢ |↑(GeneralLinearGroup.det g)| = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0

Tactic:
obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g 1

Goal state after:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) Γ(1)
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ (ConjAct.toConjAct h • 𝒢).relIndex ℋ ≠ 0

Tactic:
← ℋ.conjAct_pointwise_smul_eq_self (ℋ.le_normalizer hh),

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ (ConjAct.toConjAct h • 𝒢).relIndex (ConjAct.toConjAct h • ℋ) ≠ 0
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
hc : IsCusp ((mapGL ℝ) γ • ∞) (mapGL ℝ).range
h : ∀ (γ_1 : SL(2, ℤ)), (mapGL ℝ) γ_1 • ∞ = (mapGL ℝ) γ • ∞ → IsBoundedAtImInfty (f ∣[k] γ_1)
⊢ ((mapGL ℝ) γ • ∞).IsBoundedAt f k

Tactic:
simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using! h γ rfl

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : ⟦a⟧ = ⟦b⟧
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧

Tactic:
Quotient.eq,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : (QuotientGroup.leftRel (Subgroup.comap (mapGL ℝ) 𝒢)) a b
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧
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
⊢ ball 0 1 ∈ 𝓝 0

Tactic:
simpa [ball_zero_eq] using Metric.ball_mem_nhds (0 : ℂ) zero_lt_one

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

Goal state before:
pp: case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
⊢ (⇑f ∘ ↑ofComplex) (w + ↑h) = (⇑f ∘ ↑ofComplex) w

Tactic:
have : 0 < im (w + h) := by simp [hw]
    simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw]
    convert! SlashInvariantForm.vAdd_apply_of_mem_strictPeriods f ⟨w, hw⟩ hΓ using 2
    ext
    simp [add_comm]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_3
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
i j : Fin 2
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ i j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ i j

Tactic:
fin_cases i <;> [fin_cases j; skip]

Goal state after:
case e'_3.«0».«0»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case e'_3.«0».«1»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case e'_3.«1»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
j : Fin 2
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩) j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩) j
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))

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

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

Goal state after:
case hasSum.inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
hy' : y ≠ 0
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (↑z + ↑n).re = z.re + ↑n

Tactic:
add_re,

Goal state after:
z : ℍ
n : ℤ
⊢ (↑z).re + (↑n).re = z.re + ↑n
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 : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
hg' : ↑g 1 1 = 0
⊢ 0 = 1

Tactic:
simpa only [Matrix.det_fin_two, hg, hg', mul_zero, mul_zero, sub_zero] using g.det_coe

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 τ
τ : ℍ
g h : SL(2, ℤ)
hgh : ⟦g⟧ = ⟦h⟧
⊢ ∃ j ∈ Γ, h = g * j

Tactic:
Quotient.eq,

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 τ
τ : ℍ
g h : SL(2, ℤ)
hgh : (QuotientGroup.leftRel Γ) g h
⊢ ∃ j ∈ Γ, h = g * j
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
| fun C ↦ ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
C,

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
| fun C ↦ ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
C,

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.ModularForms.EisensteinSeries.UniformConvergence

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
⊢ ∀ (K : Set ℍ),
    IsCompact K →
      TendstoUniformlyOn (fun s x ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
        (fun x ↦ ∑' (x_1 : ↑(gammaSet N 1 a)), eisSummand k (↑x_1) x) Filter.atTop K

Tactic:
intro K hK

Goal state after:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
⊢ TendstoUniformlyOn (fun s x ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
    (fun x ↦ ∑' (x_1 : ↑(gammaSet N 1 a)), eisSummand k (↑x_1) x) Filter.atTop K
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:
norm_cast at ⊢ ht

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.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
⊢ (↑z + ↑b).re = ↑b + z.re

Tactic:
add_re,

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
⊢ (↑z).re + (↑b).re = ↑b + z.re
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this : |(↑z + ↑(↑g 1 1)).re| ≤ 1
⊢ |↑g 1 1| ≤ 1

Tactic:
add_re,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this : |(↑z).re + (↑(↑g 1 1)).re| ≤ 1
⊢ |↑g 1 1| ≤ 1
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 ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑(S • z) + ↑(↑g 0 0)).re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
add_re,

Goal state after:
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 ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑(S • z)).re + (↑(↑g 0 0)).re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ