mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h' : IsAdjoinRoot S f
map✝ : R[X] →ₐ[R] S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
eq : ∀ (x : R[X]), { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ }.map x = h'.map x
⊢ { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ } = h'

Tactic:
cases h'

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
map✝¹ : R[X] →ₐ[R] S
map_surjective✝¹ : Function.Surjective ⇑map✝¹
ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}
map✝ : R[X] →ₐ[R] S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
eq :
  ∀ (x : R[X]),
    { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹ }.map x =
      { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ }.map x
⊢ { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹ } =
    { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ }
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 : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
e : S ≃ₐ[R] T
⊢ RingHom.ker ((↑e).comp h.map) = Ideal.span {f}

Tactic:
ext; simp [Ideal.mem_span_singleton]

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
⊢ RingHom.ker (mkₐ f) = Ideal.span {f}

Tactic:
ext; simp [Ideal.mem_span_singleton]

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

Goal state before:
pp: case neg.refine_1
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
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ -↑q * z₁ + ∑ x ∈ univ \ {0, 1}, ⋯.choose ∈ ℤ[μ]

Tactic:
refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_

Goal state after:
case neg.refine_1.refine_1
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
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ ↑q ∈ ℤ[μ]

case neg.refine_1.refine_2
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
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ ∑ x ∈ univ \ {0, 1}, ⋯.choose ∈ ℤ[μ]
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    ∑ x,
      Φ x *
        (cexp (↑π * (I * s) / 2) * expZeta (toAddCircle (-x)) s + cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s)

Tactic:
map_neg,

Goal state after:
case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    ∑ x,
      Φ x *
        (cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s + cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaOdd (toAddCircle (-j)) s = -completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
map_neg,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaOdd (-toAddCircle j) s = -completedHurwitzZetaOdd (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaEven (toAddCircle (-j)) s = completedHurwitzZetaEven (toAddCircle j) s

Tactic:
map_neg,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaEven (-toAddCircle j) s = completedHurwitzZetaEven (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
← analyticOnNhd_univ_iff_differentiable

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : AnalyticOnNhd ℂ F Set.univ
hG : AnalyticOnNhd ℂ G Set.univ
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: ⊢ Summable F''

Tactic:
by
  have hp₀ (p : Nat.Primes) : 0 < (p : ℝ)⁻¹ := inv_pos_of_pos (Nat.cast_pos.mpr p.prop.pos)
  have hp₁ (p : Nat.Primes) : (p : ℝ)⁻¹ < 1 :=
    (inv_lt_one₀ <| mod_cast p.prop.pos).mpr <| Nat.one_lt_cast.mpr <| p.prop.one_lt
  suffices Summable fun (pk : Nat.Primes × ℕ) ↦ (pk.1 : ℝ)⁻¹ ^ (pk.2 + 3 / 2 : ℝ) by
    refine (Summable.mul_left 2 this).of_nonneg_of_le (fun pk ↦ ?_) (fun pk ↦ F''_le pk.1 pk.2)
    simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]
    positivity [vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))]
  conv => enter [1, pk]; rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]
  refine (summable_prod_of_nonneg (fun _ ↦ by positivity)).mpr ⟨(fun p ↦ ?_), ?_⟩
  · dsimp only -- otherwise the `exact` below times out
    exact Summable.mul_right _ <| summable_geometric_of_lt_one (hp₀ p).le (hp₁ p)
  · dsimp only
    conv => enter [1, p]; rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]
    refine (summable_rpow.mpr (by norm_num : -(3 / 2 : ℝ) < -1)).mul_left 2
      |>.of_nonneg_of_le (fun p ↦ ?_) (fun p ↦ ?_)
    · positivity [sub_pos.mpr (hp₁ p)]
    · rw [Real.inv_rpow p.val.cast_nonneg, Real.rpow_neg p.val.cast_nonneg]
      gcongr
      rw [inv_le_comm₀ (sub_pos.mpr (hp₁ p)) zero_lt_two, le_sub_comm,
        show (1 : ℝ) - 2⁻¹ = 2⁻¹ by norm_num, inv_le_inv₀ (mod_cast p.prop.pos) zero_lt_two]
      exact Nat.ofNat_le_cast.mpr p.prop.two_le

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

Goal state before:
pp: 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
hys : Summable (F y)
⊢ Tendsto (fun x ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)

Tactic:
have hc (k : ℕ) : Tendsto (F · k) atTop (nhds 0) := by
    rcases lt_or_ge (n + 1) k with H | H
    · have H₀ : (0 : ℝ) ≤ k / (n + 1) := by positivity
      have H₀' : (0 : ℝ) ≤ (n + 1) / k := by positivity
      have H₁ : (k / (n + 1) : ℂ) = (k / (n + 1) : ℝ) := by push_cast; rfl
      have H₂ : (n + 1) / k < (1 : ℝ) :=
        (div_lt_one <| mod_cast n.succ_pos.trans H).mpr <| mod_cast H
      simp only [Set.mem_ofPred_eq, H, Set.indicator_of_mem, F]
      conv =>
        enter [1, x]
        rw [div_eq_mul_inv, H₁, ← ofReal_cpow H₀, ← ofReal_inv, ← Real.inv_rpow H₀, inv_div]
      conv => enter [3, 1]; rw [← mul_zero (f k)]
      exact
        (tendsto_rpow_atTop_of_base_lt_one _ (neg_one_lt_zero.trans_le H₀') H₂).ofReal.const_mul _
    · simp [hF₀ _ H]

Goal state after:
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
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
⊢ Tendsto (fun x ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
s : ℂ
hs : 1 ≤ s.re
hs₀ : s ≠ 1
⊢ riemannZeta s ≠ 0

Tactic:
· exact LFunction_modOne_eq (χ := 1) ▸ LFunction_ne_zero_of_one_le_re _ (.inr hs₀) hs

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ LFunctionResidueClassAux a ↑x = ↑(LFunctionResidueClassAux a ↑x).re

Tactic:
eqOn_LFunctionResidueClassAux ha hx

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (fun s ↦ L (fun n ↦ ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x =
    ↑((fun s ↦ L (fun n ↦ ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x).re
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
⊢ I = ⊥

Tactic:
rw [hI, h', Ideal.span_singleton_eq_bot]

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

Goal state before:
pp: a b : ℕ
hb : Odd b
⊢ J(↑a | b) = J(↑a | b % (4 * a))

Tactic:
by
  rcases eq_or_ne a 0 with (rfl | ha₀)
  · rw [mul_zero, mod_zero]
  have hb' : Odd (b % (4 * a)) := hb.mod_even (Even.mul_right (by decide) _)
  rcases exists_eq_pow_mul_and_not_dvd ha₀ 2 (by simp) with ⟨e, a', ha₁', ha₂⟩
  have ha₁ := odd_iff.mpr (two_dvd_ne_zero.mp ha₁')
  nth_rw 2 [ha₂]; nth_rw 1 [ha₂]
  rw [Nat.cast_mul, mul_left, mul_left, quadratic_reciprocity' ha₁ hb,
    quadratic_reciprocity' ha₁ hb', Nat.cast_pow, pow_left, pow_left, Nat.cast_two, at_two hb,
    at_two hb']
  congr 1; swap
  · congr 1
    · simp_rw [qrSign]
      rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 a)]
    · rw [mod_left ↑(b % _), mod_left b, Int.natCast_mod, Int.emod_emod_of_dvd b]
      simp only [ha₂, Nat.cast_mul, ← mul_assoc]
      apply dvd_mul_left
  rcases e with - | e; · simp
  · rw [χ₈_nat_mod_eight, χ₈_nat_mod_eight (b % (4 * a)), mod_mod_of_dvd b]
    use 2 ^ e * a'; rw [ha₂, Nat.pow_succ]; ring

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

Goal state before:
pp: case inl
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : y ≤ 1
⊢ (Set.Icc x y).Finite

pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
⊢ (Set.Icc x y).Finite

Tactic:
· exact (this x).subset (Set.Icc_subset_Icc_right hy)

Goal state after:
case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
⊢ (Set.Icc x y).Finite
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsNontrivial ↔ ¬IsLocalRing.maximalIdeal ↥v.integer = ⊥

Tactic:
eq_bot_iff,

Goal state after:
K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsNontrivial ↔ ¬IsLocalRing.maximalIdeal ↥v.integer ≤ ⊥
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : 3 ^ k = -1
⊢ 1 ^ (2 * k + 1) + -(ZMod.castHom ⋯ (X q)) 1 * α = 1 - α

Tactic:
simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p : ℕ
hp : 2 ≤ p
⊢ ↑(sModNat (2 ^ p - 1) 0) = sMod p 0

Tactic:
grind [sModNat, sMod]

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

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Monoid G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ (-a) ∣[k] g + a ∣[k] g = 0

Tactic:
← add_slash,

Goal state after:
β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Monoid G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ (-a + a) ∣[k] g = 0
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ (f ∣[k] ModularGroup.S) z = f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)

Tactic:
by
  rw [SL_slash_apply, modular_S_smul]
  simp [ModularGroup.S, denom]

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
have := 𝒢.widthInfty_mem_periods

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
this : 𝒢.widthInfty ∈ 𝒢.periods
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.periods
inst✝ : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
⊢ 0 < 𝒢.widthInfty ↔ IsCusp ∞ 𝒢

Tactic:
widthInfty,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.periods
inst✝ : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
⊢ 0 < 𝒢.adjoinNegOne.strictWidthInfty ↔ IsCusp ∞ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
by
      simpa only [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
        FunLike.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]
        using (f.bdd_at_cusps' hc g hg).const_smul_left _

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k k_1 k_2 : ℤ
inst✝ : Γ.HasDetPlusMinusOne
f : ModularForm Γ k_1
g : ModularForm Γ k_2
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((f.mul g.toSlashInvariantForm).toFun ∣[k_1 + k_2] γ)

Tactic:
by
    simpa [mul_slash] using! ((f.bdd_at_cusps' hc γ hγ).mul (g.bdd_at_cusps' hc γ hγ)).smul _

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

Goal state before:
pp: case refine_2
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
⊢ ∀ ⦃x₂ : Fin 2 → ℤ⦄, x₂ ∈ gammaSet 1 r 0 → divIntMap (↑r) x = divIntMap (↑r) x₂ → x = x₂

Tactic:
v

Goal state after:
case refine_2
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
v : Fin 2 → ℤ
⊢ v ∈ gammaSet 1 r 0 → divIntMap (↑r) x = divIntMap (↑r) v → x = v
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
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
⊢ -2 * ↑π * ↑t / ↑h + ↑u * (2 * ↑π / ↑h) * Complex.I = 2 * ↑π * Complex.I * (↑u + ↑t * Complex.I) / ↑h

Tactic:
have := I_sq

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : Complex.I ^ 2 = -1
⊢ -2 * ↑π * ↑t / ↑h + ↑u * (2 * ↑π / ↑h) * Complex.I = 2 * ↑π * Complex.I * (↑u + ↑t * Complex.I) / ↑h
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic

Goal state before:
pp: k : ℤ
N : ℕ
inst✝ : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(N))
⊢ c.IsBoundedAt (⇑(eisensteinSeriesSIF a k)) k

Tactic:
by
    rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
    rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]
    exact fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeriesSIF a hk γ

Goal state after:
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 : 0 ≤ ↑g 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
have hd' : g 1 1 = 1 ∨ g 1 1 = -1 := by
    simpa [hc, isCoprime_zero_left, Int.isUnit_iff] using bottom_row_coprime g

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd : 0 ≤ ↑g 1 1
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: ⊢ symmetricIcc ℤ = symmetricIoo ℤ

Tactic:
by
  simp only [symmetricIcc, symmetricIoo, mk.injEq]
  ext s
  simp only [← Nat.map_cast_int_atTop, Filter.map_map, Filter.mem_map, mem_atTop_sets,
    Set.mem_preimage, comp_apply]
  refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩ <;>
  [convert! ha (b - 1) (by grind) using 1; convert! ha (b + 1) (by grind) using 1] <;>
  simp [Finset.ext_iff] <;> grind

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

Goal state before:
pp: z : ℂ
n : ℕ
h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (↑n + 1) * x)) = (fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (↑n + 1) * x
⊢ -1 * deriv (fun x ↦ 2 * ↑π * I * (↑n + 1) * x) z * cexp (2 * ↑π * I * (↑n + 1) * z) /
      (1 - 1 * cexp (2 * ↑π * I * (↑n + 1) * z)) =
    2 * ↑π * I * (↑n + 1) * -cexp (2 * ↑π * I * (↑n + 1) * z) / (1 - cexp (2 * ↑π * I * (↑n + 1) * z))

Tactic:
deriv_const_mul_id

Goal state after:
z : ℂ
n : ℕ
h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (↑n + 1) * x)) = (fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (↑n + 1) * x
⊢ -1 * (2 * ↑π * I * (↑n + 1)) * cexp (2 * ↑π * I * (↑n + 1) * z) / (1 - 1 * cexp (2 * ↑π * I * (↑n + 1) * z)) =
    2 * ↑π * I * (↑n + 1) * -cexp (2 * ↑π * I * (↑n + 1) * z) / (1 - cexp (2 * ↑π * I * (↑n + 1) * z))
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun x ↦ 2 * ↑π * I / ↑h * x
⊢ logDeriv cexp (2 * ↑π * I / ↑h * z) * deriv (fun x ↦ 2 * ↑π * I / ↑h * x) z = 2 * ↑π * I / ↑h

Tactic:
deriv_const_mul_id

Goal state after:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun x ↦ 2 * ↑π * I / ↑h * x
⊢ logDeriv cexp (2 * ↑π * I / ↑h * z) * (2 * ↑π * I / ↑h) = 2 * ↑π * I / ↑h
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rw [← Int.cast_one (R := ℝ), Int.cast_le] at hgzre

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : 0 ≤ ↑g 0 0 ∧ ↑g 0 0 ≤ 1
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = 1
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
n : ℕ
this : ∀ (x : ℂ), cexp (2 * ↑π * I * ↑n * x / 1) = cexp (2 * ↑π * I * x / 1) ^ n
⊢ iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z = (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
simp_rw [div_one] at this

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 : ℕ
this : ∀ (x : ℂ), cexp (2 * ↑π * I * ↑n * x) = cexp (2 * ↑π * I * x) ^ n
⊢ iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z = (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n