mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case zero
⊢ 0 = log (0 + 1) - ↑(0 + (↑(0 + 1))⁻¹) + 1

Tactic:
zero_add,

Goal state after:
case zero
⊢ 0 = log 1 - ↑(↑1)⁻¹ + 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x / y) = logHeight ![x, y]

Tactic:
by
  rw [logHeight₁_eq_log_mulHeight₁, logHeight_eq_log_mulHeight, mulHeight₁_div_eq_mulHeight x y]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ ^ 2 * ↑S.u₄ * S.Z ^ 3 = S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3

Tactic:
by simp [← Units.val_pow_eq_pow_val, S.u₄_sq]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ (h.basis.repr (h.root ^ n)) ⟨i, hi⟩ = (h.basis.repr (h.basis ⟨n, hn⟩)) ⟨i, hi⟩

Tactic:
rw [h.basis_apply, Fin.val_mk]

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

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
classical
    rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst✝¹ : Module.Finite R S
inst✝ : Free R S
α : S
hα : (aeval α).range = ⊤
monic : (minpoly R α).Monic
this✝ : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
φ : AdjoinRoot (minpoly R α) →ₐ[R] S := AdjoinRoot.liftAlgHom (minpoly R α) (Algebra.ofId R S) α ⋯
s : S
⊢ ∃ a, φ.toLinearMap a = s

Tactic:
AlgHom.range_eq_top

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst✝¹ : Module.Finite R S
inst✝ : Free R S
α : S
hα : Function.Surjective ⇑(aeval α)
monic : (minpoly R α).Monic
this✝ : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
φ : AdjoinRoot (minpoly R α) →ₐ[R] S := AdjoinRoot.liftAlgHom (minpoly R α) (Algebra.ofId R S) α ⋯
s : S
⊢ ∃ a, φ.toLinearMap a = s
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Tactic:
by
  have := isDomain_of_prime (prime_of_isIntegrallyClosed hx')
  have :=
    noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx')
      (degree_pos hx').ne'
  rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]

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

Goal state before:
pp: case inl
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
have hχ : changeLevel hMN χ ≠ 1 := h ∘ (changeLevel_eq_one_iff hMN).mp
    have h' : Continuous fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * ↑p ^ (-s)) :=
      (differentiable_LFunction h).continuous.mul <| continuous_finsetProd _ fun p hp ↦ by
        have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
        fun_prop
    exact congrFun ((differentiable_LFunction hχ).continuous.ext_on
      (dense_compl_singleton 1) h' (fun _ h ↦ LFunction_changeLevel_aux hMN χ h)) s

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

Goal state before:
pp: case refine_2
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
· push_cast
      congr 1
      have : (Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ) = _ :=
        (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm
      rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]
      apply Polynomial.map_aeval_eq_aeval_map (by simp)

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
⊢ 0 + hurwitzZetaOdd (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
zero_add,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
⊢ hurwitzZetaOdd (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (-↑k) =
    -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))

Tactic:
rcases Nat.even_or_odd' k with ⟨n, (rfl | rfl)⟩
  · exact_mod_cast hurwitzZeta_neg_two_mul_nat (by lia : n ≠ 0) hx
  · exact_mod_cast hurwitzZeta_one_sub_two_mul_nat (by lia : n + 1 ≠ 0) hx

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
⊢ Summable fun n ↦ -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
have :
      ∀ n : ℤ, -(k ! : ℂ) / (2 * π * I * n) ^ k = -k ! / (2 * π * I) ^ k * (1 / (n : ℂ) ^ k) := by
    intro n; rw [mul_one_div, div_div, ← mul_pow]

Goal state after:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n ↦ -↑k ! / (2 * ↑π * I * ↑n) ^ k
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inl
⊢ -1 / 2 = -↑(bernoulli' (0 + 1)) / (0 + 1)

Tactic:
zero_add,

Goal state after:
case inl
⊢ -1 / 2 = -↑(bernoulli' 1) / (0 + 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inl
⊢ -1 / 2 = -↑(bernoulli' 1) / (0 + 1)

Tactic:
zero_add,

Goal state after:
case inl
⊢ -1 / 2 = -↑(bernoulli' 1) / 1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr.refine_2.hf
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt G 1

Tactic:
simpa only [G, continuousAt_update_same] using riemannZeta_residue_one

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2 * (0 + 1)) = 0
⊢ B.F ↑(-2) = 0

Tactic:
zero_add,

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2 * 1) = 0
⊢ B.F ↑(-2) = 0
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ ‖↑a * z ^ 2‖ < 1

Tactic:
rwa [norm_mul, norm_pow, hz, one_pow, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)

Tactic:
· rw [pow_add, pow_one]
      conv_rhs =>
        rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_mul, I_sq]
      ring

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

Goal state before:
pp: case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤

Tactic:
· simp only [h, or_false]
    refine ⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩
    convert! (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h
    · refine ⟨fun H' _ _ ↦ by rw [H', Pi.zero_apply], fun H' ↦ ?_⟩
      ext (- | m)
      · simp [hf]
      · simp [H']
    · simpa only [H] using! Filter.EventuallyEq.rfl

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ 0 + ∑ x ∈ Icc (0 + 1) n, f x = ∑ k ∈ Icc 1 n, f k

Tactic:
zero_add,

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ ∑ x ∈ Icc (0 + 1) n, f x = ∑ k ∈ Icc 1 n, f k
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
x✝ : ℤ
⊢ x✝ ∈ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯ →
    x✝ ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
ha'

Goal state after:
a : ℤ
b : ℕ
x✝ : ℤ
ha' : x✝ ∈ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯
⊢ x✝ ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n = (-1) ^ (m / 2 * (n / 2))

Tactic:
rw [qrSign, pow_mul, ← χ₄_eq_neg_one_pow (odd_iff.mp hm)]

Goal state after:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)
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:
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ε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ ‖((↑s - 1) * ↑s * ∫ (t : ℝ) in Set.Ioi 1, S t * ↑t ^ (-↑s - 1)) -
        l * ↑s * ((↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s))‖ =
    ‖(↑s - 1) * ↑s * ∫ (t : ℝ) in Set.Ioi 1, S t * ↑t ^ (-↑s - 1) - l * ↑t ^ (-↑s)‖

Tactic:
by
      rw [integral_sub, integral_const_mul]
      · congr; ring
      · exact (lemma₁ hlim hs).mono_set Set.Ioi_subset_Ici_self
      · exact (integrableOn_Ioi_cpow_of_lt
          (by rwa [neg_re, ofReal_re, neg_lt_neg_iff]) zero_lt_one).const_mul _

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ sZMod (p' + 2) (p' + 2 - 2) = 0

Tactic:
sZMod_eq_s p',

Goal state after:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ ↑(s (p' + 2 - 2)) = 0
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
hn : g ^ (-1) < g ^ n
⊢ g ^ n < g ^ 1 → ⟨g ^ n, ⋯⟩ = 1

Tactic:
hn'

Goal state after:
case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
hn : g ^ (-1) < g ^ n
hn' : g ^ n < g ^ 1
⊢ ⟨g ^ n, ⋯⟩ = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 1

Tactic:
simpa [ConjAct.smul_def] using HasDetOne.det_eq hh

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

Goal state before:
pp: N : ℕ
g : ConjAct SL(2, ℤ)
⊢ g • Γ(N) = Γ(N)

Tactic:
apply Subgroup.Normal.conjAct (Gamma_normal N)

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:
mul_comm a₁ a₂,

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.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⁻¹ * (0 + (↑z * ↑(c 1)).im) = c 1

Tactic:
zero_add,

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 * ↑(c 1)).im = c 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
⊢ ↑(g • z) =
    ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))

Tactic:
have nonZ1 : (p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2 ≠ 0 := mod_cast hp.sq_add_sq_ne_zero

Goal state after:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
⊢ ↑(g • z) =
    ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hc
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

Tactic:
· exact normSq_denom_pos g z.im_ne_zero

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

Goal state before:
pp: case pos
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : r = 0
⊢ v = r • divIntMap (↑r) v

pp: case neg
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
⊢ v = r • divIntMap (↑r) v

Tactic:
· have hv := hv.2
    simp only [hr, Fin.isValue, Int.gcd_eq_zero_iff, CharP.cast_eq_zero, zero_smul] at *
    ext i
    fin_cases i <;> simp [hv]

Goal state after:
case neg
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
⊢ v = r • divIntMap (↑r) v
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
⊢ (∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖) →
    ‖(PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)‖ ≤ 1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖

Tactic:
hn'

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ ‖(PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)‖ ≤ 1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
⊢ D (F ∣[k] g) = fun z ↦
    (↑(↑g).det)⁻¹ * (D F ∣[k + 2] g) z - ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F ∣[k] g) z

Tactic:
by
  have hdet : g.det.val = g.val.det := Matrix.GeneralLinearGroup.val_det_apply g
  have hdetℂ : (g.val.det : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr hg.ne'
  have hσ (x) : σ g x = x := by grind [σ, ContinuousAlgEquiv.refl_apply]
  ext z
  simp only [normalizedDerivOfComplex, ModularForm.slash_apply]
  have hz := denom_ne_zero g z
  have h_smul : HasDerivAt (fun w ↦ ↑(g • ofComplex w) : ℂ → ℂ)
      ((g.val.det : ℂ) / denom g z ^ 2) ↑z := (hasStrictDerivAt_smul hg z).hasDerivAt
  have h_F : HasDerivAt (F ∘ ofComplex) (deriv (F ∘ ofComplex) ↑(g • ofComplex (z : ℂ)))
      ↑(g • ofComplex (z : ℂ)) :=
    (ofComplex_apply z).symm ▸ (mdifferentiableAt_iff.mp (hF (g • z))).hasDerivAt
  have h_denom : HasDerivAt (fun w ↦ (denom g w) ^ (-k))
      (-k * (g 1 0 : ℂ) * (denom g z) ^ (-k - 1)) ↑z := by
    simpa using hasDerivAt_denom_zpow g (-k) z
  have hcomp : ((F ∣[k] g) ∘ ofComplex) =ᶠ[𝓝 ↑z]
      fun w ↦ (g.val.det : ℂ) ^ (k - 1) *
        ((F ∘ ofComplex) ↑(g • ofComplex w) * (denom g w) ^ (-k)) := by
    filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds z.im_pos] with w hw
    grind [ofComplex_apply_of_im_pos, ofComplex_apply, ModularForm.slash_apply]
  rw [((((h_F.comp (z : ℂ) h_smul).mul h_denom).const_mul _).congr_of_eventuallyEq hcomp).deriv]
  simp only [hσ, hdet, abs_of_pos hg, ofComplex_apply, Function.comp_apply]
  rw [show k + 2 - 1 = (k - 1) + 2 by ring, show -(k + 2) = -k + -2 by ring,
    zpow_add₀ hdetℂ, zpow_add₀ hz, zpow_sub_one₀ hz]
  field

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
z : ℍ
hLHS :
  (serreDerivative (↑k) F ∣[k + 2] γ) z =
    (D F ∣[k + 2] γ) z - ↑k * 12⁻¹ * ((EisensteinSeries.E2 ∣[2] γ) z * (F ∣[k] γ) z)
hDz :
  D (F ∣[k] γ) z =
    (D F ∣[k + 2] γ) z -
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑γ 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] γ) z
hE2z : (EisensteinSeries.E2 ∣[2] γ) z = EisensteinSeries.E2 z - 1 / (2 * riemannZeta 2) * EisensteinSeries.D2 γ z
⊢ (serreDerivative (↑k) F ∣[k + 2] γ) z = serreDerivative (↑k) (F ∣[k] γ) z

Tactic:
grind [serreDerivative_apply, EisensteinSeries.D2, riemannZeta_two, I_sq]

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

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ * (↑π * I / 12) =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z

Tactic:
hE2,

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)) * (↑π * I / 12) =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rw [show S * T⁻¹ = ⟨!![0, -1; 1, -1], by simp⟩ by decide]

Goal state after:
case inr.inr.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(S * T⁻¹) 1 0
hc : ↑(S * T⁻¹) 1 0 = 1
hd : ↑(S * T⁻¹) 1 1 = -1
hz : 1 +ᵥ ρ ∈ 𝒟
hg : (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) ⟨!![0, -1; 1, -1], ⋯⟩)) ↑(1 +ᵥ ρ)) = 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
have := tsum_prod_pow_eq_tsum_sigma 1 (norm_exp_two_pi_I_lt_one z)

Goal state after:
z : ℍ
this :
  ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ 1 * cexp (2 * ↑π * I * ↑z) ^ (↑d * ↑c) =
    ∑' (e : ℕ+), ↑((σ 1) ↑e) * cexp (2 * ↑π * I * ↑z) ^ ↑e
⊢ -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)