mathlib-initiative/mathlib-tactics huggingface dataset:
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
x y : S
| h.repr (h.map (h.repr x) + h.map (h.repr y)) %ₘ f

Tactic:
← map_add,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
| h.repr (h.map (h.repr x + h.repr y)) %ₘ f
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
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff ↑i = g i

Tactic:
rw [Finsupp.mapDomain_apply Fin.val_injective]

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
⊢ (Finsupp.single ⟨n, hn⟩ 1) ⟨i, hi⟩ = Pi.single (↑⟨n, hn⟩) 1 ↑⟨i, ?m.131⟩

Tactic:
← Finsupp.single_eq_pi_single,

Goal state after:
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
⊢ (Finsupp.single ⟨n, hn⟩ 1) ⟨i, hi⟩ = (Finsupp.single (↑⟨n, hn⟩) 1) ↑⟨i, ?m.131⟩
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C₁ : ℝ
hC₁ : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C₁ + logHeight ![a, b] + logHeight ![c, d]
C₂ : ℝ
hC₂ :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ |logHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝] - (logHeight ![a✝, b✝] + logHeight ![c✝, d✝])| ≤ max C₁ (-C₂)

Tactic:
by specialize hC₂ hab hcd; grind

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1))

Tactic:
by
    rw [completedLFunction, completedLFunction_const_mul]
    ring

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

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
hw : 1 ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ LFunctionTrivChar₁ n 1 ≠ 0

pp: case inr
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
hw' : w ≠ 1
⊢ LFunctionTrivChar₁ n w ≠ 0

Tactic:
· exact LFunctionTrivChar₁_apply_one_ne_zero _

Goal state after:
case inr
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
hw' : w ≠ 1
⊢ LFunctionTrivChar₁ n w ≠ 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
by
  let U := if j = 0 then {z : ℂ | z ≠ 1} else univ -- region of analyticity of both functions
  let V := {z : ℂ | 1 < re z} -- convergence region
  have hUo : IsOpen U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using! isOpen_compl_singleton
    · simp only [h, ↓reduceIte, isOpen_univ, U]
  let f := LFunction (fun k ↦ stdAddChar (j * k))
  let g := expZeta (toAddCircle j)
  have hU {u} : u ∈ U ↔ u ≠ 1 ∨ j ≠ 0 := by simp only [mem_ite_univ_right, U]; tauto
  -- hypotheses for uniqueness of analytic continuation
  have hf : AnalyticOnNhd ℂ f U := by
    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
    refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
    simp only [mul_comm j, AddChar.sum_mulShift _ (isPrimitive_stdAddChar _), h,
      ↓reduceIte, CharP.cast_eq_zero]
  have hg : AnalyticOnNhd ℂ g U := by
    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
    refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
    rwa [ne_eq, toAddCircle_eq_zero]
  have hUc : IsPreconnected U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using!
        (isConnected_compl_singleton_of_one_lt_rank (by simp) _).isPreconnected
    · simpa only [h, ↓reduceIte, U] using isPreconnected_univ
  have hV : V ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
  have hUmem : 2 ∈ U := by simp [U]
  have hUmem' : s ∈ U := hU.mpr hjs.symm
  -- apply uniqueness result
  refine hf.eqOn_of_preconnected_of_eventuallyEq hg hUc hUmem ?_ hUmem'
  -- now remains to prove equality on `1 < re s`
  filter_upwards [hV] with z using LFunction_stdAddChar_eq_expZeta_of_one_lt_re _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ ∫ (x : ℝ) in 0..1, bernoulliFun k x = 0

Tactic:
integral_bernoulliFun,

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ (if k = 0 then 1 else 0) = 0
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
apply DifferentiableAt.congr_of_eventuallyEq
  · exact (differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)
  · filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_of_ne ht ..

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

Goal state before:
pp: case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

Tactic:
· exact (LSeriesSummable_congr _ fun h ↦ (B.χ.apply_eq_toArithmeticFunction_apply h).symm).mpr <|
      ZMod.LSeriesSummable_of_one_lt_re B.χ hs

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

Goal state before:
pp: case neg
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
hm : m ≤ n + 1
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m

Tactic:
· simp [hm, hF₀ _ hm]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two]

Goal state after:
case e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(1 / 6) / ↑2!
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
hr : ¬r = 0
x : K
hx : (valuation K) x ≤ (valuation K) r ^ 2
⊢ (valuation K) x < (valuation K) r

Tactic:
exact hx.trans_lt (by simpa [pow_two, hr])

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := fun n ↦ f n +ᵥ ↑(𝓂[K] ^ n)
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
⊢ ∀ (i : ℕ), (S i).Nonempty

Tactic:
by simp [S]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ J(a | p) = fastLegendreSym p a

Tactic:
fastLegendreSym

Goal state after:
p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ J(a | p) = J(a | p)
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∀ {x_1 y : A},
    (x_1 ∈ Set.range fun x_2 ↦ x * x_2) → (y ∈ Set.range fun x_2 ↦ x * x_2) → x_1 + y ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨x + y, mul_add _ _ _⟩

Goal state after:
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 Γ₀
hc : IsCompact ↑𝒪[K]
val✝ : LocallyFiniteOrder (↥(MonoidHom.mrange v))ˣ
⊢ MulArchimedean (↥(MonoidHom.mrange v))ˣ

Tactic:
exact MulArchimedean.of_locallyFiniteOrder

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

Goal state before:
pp: case refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : CompactSpace ↥𝒪[K]
⊢ CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]

Tactic:
have : IsDiscreteValuationRing 𝒪[K] := isDiscreteValuationRing_of_compactSpace

Goal state after:
case refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : CompactSpace ↥𝒪[K]
this : IsDiscreteValuationRing ↥𝒪[K]
⊢ CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
x✝ : CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]
left✝¹ : CompleteSpace ↥𝒪[K]
left✝ : IsDiscreteValuationRing ↥𝒪[K]
h : TotallyBounded Set.univ
⊢ TotallyBounded Set.univ ∧ IsComplete Set.univ

Tactic:
exact ⟨h, completeSpace_iff_isComplete_univ.mp ‹_›⟩

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_1
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑(boxPoly n B₁ B₂)
prop : ∀ (i : Fin (n + 1)), B₁ i ≤ ↑((↑p).coeff ↑i) ∧ ↑((↑p).coeff ↑i) ≤ B₂ i
⊢ (toFn (n + 1)) ↑p ∈ ↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)

Tactic:
simpa using ⟨fun i ↦ ceil_le.mpr (prop i).1, fun i ↦ le_floor.mpr (prop i).2⟩

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
⊢ ∃ n, 0 < n ∧ cyclotomic n ℤ ∣ p

Tactic:
have hpdegC : (p.map (castRingHom ℂ)).degree ≠ 0 := by
    rwa [p.degree_map_eq_of_injective (castRingHom ℂ).injective_int]

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
⊢ ∃ n, 0 < n ∧ cyclotomic n ℤ ∣ p
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)
Γ : Subgroup (SL n R)
g : GL n R
hg : g ∈ map toGL Γ
⊢ GeneralLinearGroup.det g = 1

Tactic:
by rcases hg with ⟨g, hg, rfl⟩; simp

Goal state after:
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)
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
Γ : Subgroup (SL n R)
g : GL n S
hg : g ∈ map (mapGL S) Γ
⊢ GeneralLinearGroup.det g = 1

Tactic:
by rcases hg with ⟨g, hg, rfl⟩; simp

Goal state after:
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)
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : GL n S
hg : g ∈ (mapGL S).range
⊢ GeneralLinearGroup.det g = 1

Tactic:
by rcases hg with ⟨g, hg, rfl⟩; simp

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

Goal state before:
pp: N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N

Tactic:
simp only [Gamma0_mem, Gamma1_mem] at *

Goal state after:
N : ℕ
x : SL(2, ℤ)
HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0
⊢ ↑(↑x 1 0) = 0
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
⊢ OnePoint K

Tactic:
by
    refine Projectivization.lift
      (fun u : {v : Fin 2 → K // v ≠ 0} ↦ if u.1 1 = 0 then ∞ else ((u.1 1)⁻¹ * u.1 0)) ?_ p
    rintro ⟨-, hv⟩ ⟨w, hw⟩ t rfl
    have ht : t ≠ 0 := by rintro rfl; simp at hv
    by_cases h₀ : w 1 = 0 <;> simp [h₀, ht, mul_assoc]

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

Goal state before:
pp: 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) ≤ (mapGL ℝ).range
k : SL(2, ℤ)
⊢ k ∈ Γ(N) → k ∈ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)

Tactic:
hk

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) ≤ (mapGL ℝ).range
k : SL(2, ℤ)
hk : k ∈ Γ(N)
⊢ k ∈ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
c : OnePoint ℝ
⊢ IsCusp c (mapGL ℝ).range → c ∈ Set.range (OnePoint.map Rat.cast)

pp: case mpr
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → IsCusp c (mapGL ℝ).range

Tactic:
· rintro ⟨-, ⟨g, rfl⟩, hgp, hgc⟩
    simpa only [hgp.smul_eq_self_iff.mp hgc] using ⟨(mapGL ℚ g).parabolicFixedPoint,
      by simp [GeneralLinearGroup.parabolicFixedPoint, apply_ite]⟩

Goal state after:
case mpr
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → IsCusp c (mapGL ℝ).range
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ‖0‖ ≤ rexp (-π)

Tactic:
by simpa only [norm_zero] using exp_nonneg _

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

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
⊢ BijOn (divIntMap ↑r) (gammaSet 1 r 0) (gammaSet 1 1 0)

Tactic:
refine ⟨?_, ?_, ?_⟩

Goal state after:
case refine_1
r : ℕ
inst✝ : NeZero r
⊢ MapsTo (divIntMap ↑r) (gammaSet 1 r 0) (gammaSet 1 1 0)

case refine_2
r : ℕ
inst✝ : NeZero r
⊢ InjOn (divIntMap ↑r) (gammaSet 1 r 0)

case refine_3
r : ℕ
inst✝ : NeZero r
⊢ SurjOn (divIntMap ↑r) (gammaSet 1 r 0) (gammaSet 1 1 0)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case pos
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
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ max τ.im (1 / τ.im)

Tactic:
have : g 1 1 ≠ 0 := fun hg' ↦ zero_ne_one <| by
      simpa only [Matrix.det_fin_two, hg, hg', mul_zero, mul_zero, sub_zero] using g.det_coe
    have : (1 : ℝ) ≤ g 1 1 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs this)
    refine le_trans ?_ <| le_max_left _ _
    rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) = (g 1 1) ^ 2 by simp [hg, sq]]
    simpa [field] using inv_le_one_of_one_le₀ this

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 : ℕ
⊢ ∑' (n : ℕ+), ↑↑n ^ k * r ^ ↑n / (1 - r ^ ↑n) = ∑' (n : ℕ+), ↑((σ k) ↑n) * r ^ ↑n

Tactic:
have (m : ℕ) [NeZero m] := tsum_geometric_of_norm_lt_one (ξ := r ^ m)
    (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
  simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (f := fun m ↦ n ^ k * (r ^ n) ^ m)]
  have h00 := tsum_prod_pow_eq_tsum_sigma k hr
  rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00
  rw [← h00]
  exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm c.val b.val, pow_mul]

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
this : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : √(normSq (↑z - 1)) ≤ 1
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = 1 +ᵥ ρ

Tactic:
Real.sqrt_le_one

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq (↑z - 1) ≤ 1
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F - G) = D F - D G

Tactic:
ext z
  have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
  have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
  simp only [normalizedDerivOfComplex, Pi.sub_apply]
  rw [show (F - G) ∘ ofComplex = F ∘ ofComplex - G ∘ ofComplex from rfl,
    deriv_sub hFz hGz, mul_sub]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ z.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = z.im

Tactic:
div_eq_iff (normSq_denom_pos _ z.im_ne_zero).ne',

Goal state after:
case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ z.im = z.im * normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)
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)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = ↑z ^ (-1 / 2) / 2 * (↑z ^ 2⁻¹)⁻¹ + ↑π * I / 12 * E2 z

Tactic:
rw [div_mul_eq_mul_div₀ _ _ (2 : ℂ), neg_div, cpow_neg, ← mul_inv, ← cpow_add _ _ z.ne_zero]

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)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = (↑z ^ (1 / 2 + 2⁻¹))⁻¹ / 2 + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hg
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet

Tactic:
exact fun x hx ↦ ((differentiableAt_sqrt (mem_slitPlane ⟨x, hx⟩)).mul
     (differentiableAt_eta_of_mem_upperHalfPlaneSet hx)).differentiableWithinAt

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

Goal state before:
pp: htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1))) ^ 24) atImInfty (𝓝 1)
⊢ Tendsto (fun x ↦ ∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1)) ^ 24) atImInfty (𝓝 1)

Tactic:
convert! this using 2 with τ

Goal state after:
htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1))) ^ 24) atImInfty (𝓝 1)
τ : ℍ
⊢ ∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑τ) ^ (n + 1)) ^ 24 = (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑τ) ^ (n + 1))) ^ 24
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
⊢ ∀ᶠ (x : ℍ) in atImInfty, ‖rexp (-2 * π * x.im)‖ ≤ 2 * ‖Δ x‖

Tactic:
filter_upwards [hprod] with τ hτ

Goal state after:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
τ : ℍ
hτ : dist (∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24) 1 < 1 / 2
⊢ ‖rexp (-2 * π * τ.im)‖ ≤ 2 * ‖Δ τ‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

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

Tactic:
rw [sum_Icc_of_even_eq_range (e2Summand_even z), Finset.sum_range_succ', smul_add,
    nsmul_eq_mul, Nat.cast_zero, e2Summand_zero_eq_two_riemannZeta_two]
  ring_nf
  simp only [e2Summand, eisSummand, add_comm, Nat.cast_add, Nat.cast_one, Fin.isValue,
    Matrix.cons_val_zero, Int.cast_add, Int.cast_natCast, Int.cast_one, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, mul_comm, mul_sum]
  congr with a
  have H2 := qExpansion_identity_pnat (k := 1) (by grind)
    ⟨(a + 1) * z, by simpa [show 0 < ((a + 1) : ℝ) by positivity] using z.2⟩
  simp only [add_comm, Nat.reduceAdd, one_div, mul_comm, mul_neg, even_two,
    Even.neg_pow, Nat.factorial_one, Nat.cast_one, div_one, pow_one] at H2
  simp_rw [zpow_ofNat, H2, ← tsum_mul_left, ← tsum_neg, ← exp_nsmul]
  refine tsum_congr fun b ↦ ?_
  ring_nf
  grind [I_sq, exp_add]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : z.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = z.im
hc : 0 ≤ ↑g 1 0
⊢ (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:
div_eq_iff (normSq_denom_pos _ z.im_ne_zero).ne',

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : z.im = z.im * normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)
hc : 0 ≤ ↑g 1 0
⊢ (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 = ρ