mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
rcases HZ with ⟨Z, hZ⟩

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -2 + 1 = -1

Tactic:
by norm_num

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
a b : { v // v ≠ 0 }
t : K
h : ↑a = t • ↑b
⊢ t ≠ 0

Tactic:
contrapose! h

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
a b : { v // v ≠ 0 }
t : K
h : t = 0
⊢ ↑a ≠ t • ↑b
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∃ z ∈ ℤ[μ], ↑(m + k + 1) = z * (μ - 1) ^ k

Tactic:
refine ⟨(-1) ^ (m + k) * (∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1),
    ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1) ∈ ℤ[μ]

case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ↑(m + k + 1) = (((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ 2 / 3 < 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ 2.7182818286 < 4 * 2

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 2 ∈ {1}ᶜ

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 2 ∈ {b | 1 < b.re}

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case inr
s : ℂ
hs : s ≠ 1
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)

Tactic:
· -- `conj ∘ ζ ∘ conj` is analytic on `{1}ᶜ` and agrees with `ζ` termwise on `1 < re z`, so
    -- the identity principle propagates the equality to the connected set `{1}ᶜ`.
    have hg_an : AnalyticOnNhd ℂ (fun z ↦ conj (riemannZeta (conj z))) {1}ᶜ :=
      DifferentiableOn.analyticOnNhd
        (fun z hz ↦ (differentiableAt_conj_conj_iff.mpr <| differentiableAt_riemannZeta <|
          (map_ne_one_iff _ (starRingEnd ℂ).injective).mpr hz).differentiableWithinAt)
        isOpen_compl_singleton
    have hgz (z : ℂ) (hz : 1 < z.re) : conj (riemannZeta (conj z)) = riemannZeta z := by
      rw [zeta_eq_tsum_one_div_nat_cpow (by rwa [conj_re]), conj_tsum,
        zeta_eq_tsum_one_div_nat_cpow hz]
      exact tsum_congr fun n ↦ by
        rw [map_div₀, map_one, ← conj_cpow _ _ (by rw [natCast_arg]; positivity), conj_natCast]
    have heq : EqOn (fun z ↦ conj (riemannZeta (conj z))) riemannZeta {1}ᶜ :=
      hg_an.eqOn_of_preconnected_of_eventuallyEq analyticOn_riemannZeta
        (isConnected_compl_singleton_of_one_lt_rank (by simp) 1).isPreconnected
        (by norm_num : (2 : ℂ) ∈ _)
        (eventuallyEq_of_mem
          ((isOpen_lt continuous_const continuous_re).mem_nhds (by norm_num)) hgz)
    simpa using congrArg (starRingEnd ℂ) (heq hs)

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
⊢ mulHeight (Int.cast ∘ x) = ↑(⨆ i, |x i|)

Tactic:
by
  have hx₀ : Int.cast ∘ x ≠ (0 : ι → ℚ) := by
    contrapose! hx
    rw [Function.comp_eq_zero_iff x intCast_injective Rat.intCast_zero] at hx
    rw [hx, Finset.gcd_eq_zero_iff.mpr (by simp)]
    exact zero_ne_one
  simp_rw [Finite.map_iSup_of_monotone _ Int.cast_mono, NumberField.mulHeight_eq hx₀,
    infinitePlace_apply]
  simp [finprod_eq_one_of_forall_eq_one (iSup_finitePlace_apply_eq_one_of_gcd_eq_one · hx)]

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

Goal state before:
pp: case e'_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ↑(max q.num.natAbs q.den) = ↑(⨆ i, |![q.num, ↑q.den] i|)

Tactic:
rw [← Int.cast_natCast, Int.cast_inj]
    push_cast
    refine le_antisymm (max_le ?_ ?_) <| ciSup_le fun i ↦ ?_
    · exact Finite.le_ciSup_of_le 0 <| by simp
    · exact Finite.le_ciSup_of_le 1 <| by simp
    · fin_cases i <;> simp

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:
rw [completedLFunction, completedLFunction_const_mul]

Goal state after:
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) / ε * (χ⁻¹ (-1) * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s * (χ (-1) * χ⁻¹ (-1))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∑ i ∈ Finset.range m, ∫ (x : ℝ) in 0..(↑m)⁻¹, bernoulliFun (k + 1) (x + ↑i / ↑m) = 0

Tactic:
simp only [intervalIntegral.integral_comp_add_right, zero_add, ← one_div, ← add_div,
            add_comm (1 : ℝ), ← Nat.cast_add_one]
          rw [intervalIntegral.sum_integral_adjacent_intervals]
          · simp [div_self m0', integral_bernoulliFun_eq_zero]
          · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 2 * ↑k ≠ -↑n

Tactic:
refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt (mul_pos two_pos ?_))

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 0 < ↑k
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
⊢ ∀ (x : ℝ), f k x = 0

Tactic:
induction k with

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
n : ℕ
⊢ LFunction Φ (-(2 * (↑n + 1))) = 0

Tactic:
by
  simp only [LFunction_def_even hΦ, hurwitzZetaEven_neg_two_mul_nat_add_one, mul_zero,
    sum_const_zero, ← neg_mul]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
⊢ 0 = -↑k ! / 0 ^ k

Tactic:
zero_pow hk,

Goal state after:
case inl
k : ℕ
hk : k ≠ 0
⊢ 0 = -↑k ! / 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
have hs₁ : s ≠ 1 := (lt_irrefl _ <| one_re ▸ · ▸ hs)

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / (2 * I) - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    -I⁻¹ * LFunction (𝓕 Φ) s

Tactic:
simp only [hΦ _, neg_mul, sum_neg_distrib, LFunction_dft Φ (.inl hΦ.map_zero)]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (-∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    -(I⁻¹ * ∑ x, Φ x * expZeta (toAddCircle (-x)) s)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

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

Tactic:
exact LSeries_congr B.χ.apply_eq_toArithmeticFunction_apply s

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ Differentiable ℂ B.F

Tactic:
by
  intro s
  rcases ne_or_eq s 1 with hs | rfl
  · exact B.F_differentiableAt_of_ne hs
  -- now need to deal with `s = 1`
  refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt
  · filter_upwards [self_mem_nhdsWithin] with t ht
    exact B.F_differentiableAt_of_ne ht
  -- now reduced to showing *continuity* at s = 1
  let G := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
  let H := Function.update (fun s ↦ (B.χ.LFunction s - B.χ.LFunction 1) / (s - 1)) 1
    (deriv B.χ.LFunction 1)
  have : B.F = G * H := by
    ext1 t
    rcases eq_or_ne t 1 with rfl | ht
    · simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_self]
    · simp only [F, G, H, Function.update_of_ne ht, mul_comm _ (riemannZeta _), B.hχ, sub_zero,
      Pi.mul_apply, mul_assoc, mul_div_cancel₀ _ (sub_ne_zero.mpr ht)]
  rw [this]
  apply ContinuousAt.mul
  · simpa only [G, continuousAt_update_same] using riemannZeta_residue_one
  · exact (B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div

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

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ -(3 / 2) < -1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial (ValueGroupWithZero R)ˣ
hM : MulArchimedean (ValueGroupWithZero R)
H : DenselyOrdered (ValueGroupWithZero R)
x : ValueGroupWithZero R
hx : x < 1
hx' : ∀ δ < 1, δ ≤ x
⊢ False

Tactic:
obtain ⟨y, hy, hy'⟩ := exists_between hx

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial (ValueGroupWithZero R)ˣ
hM : MulArchimedean (ValueGroupWithZero R)
H : DenselyOrdered (ValueGroupWithZero R)
x : ValueGroupWithZero R
hx : x < 1
hx' : ∀ δ < 1, δ ≤ x
y : ValueGroupWithZero R
hy : x < y
hy' : y < 1
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Tactic:
contrapose! h

Goal state after:
case inr
a : ℤ
b : ℕ
h✝ : NeZero b
h : J(a | b) = 0
⊢ a.gcd ↑b ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Tactic:
· contrapose! h; exact eq_zero_iff_not_coprime.1 h

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✝ : IsValuativeTopology R
⊢ ∀ (x : R), Tendsto (⇑v) (𝓝 x) (𝓝 (v x))

Tactic:
rintro x

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
x : R
⊢ Tendsto (⇑v) (𝓝 x) (𝓝 (v x))
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case pos
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : v c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hcj : v j ≤ ↑↑z
hj' : c ∈ {w | v w ≤ ↑↑z}
⊢ (if hi' : v j ≤ ↑↑z then z else Units.mk0 ⟨v j, ⋯⟩ ⋯) = i

Tactic:
simp only [Set.mem_ofPred_eq, hc, Subtype.coe_le_coe, Units.val_le_val] at hj'

Goal state after:
case pos
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : v c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hcj : v j ≤ ↑↑z
hj' : i ≤ z
⊢ (if hi' : v j ≤ ↑↑z then z else Units.mk0 ⟨v j, ⋯⟩ ⋯) = i
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ 3 % 4 = 3

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

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

Tactic:
grind [Polynomial.natDegree_map_le]

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
this : X.ω ^ (2 ^ p' * 4 / 4) + X.ωb ^ (2 ^ p' * 4 / 4) = 0
⊢ 4 ≠ 0

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
induction k with

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q k : ℕ
⊢ sModNatAux (4 % q) q k = sModNat q k

Tactic:
induction k with

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q✝ i q k b : ℕ
⊢ sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q

Tactic:
induction k with

Goal state after:
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 : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1) → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1}

pp: case inr.mpr
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 : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1} → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1)

Tactic:
· simp only [Set.mem_preimage, Set.mem_Ioo, Set.mem_singleton_iff, and_imp]
    intro hn hn'
    rw [zpow_lt_zpow_iff_right ha] at hn hn'
    simp only [Subtype.ext_iff, show n = 0 by lia, zpow_zero, coe_one]

Goal state after:
case inr.mpr
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 : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1} → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1)
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ,
      toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) y) =
        toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) * toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) x) *
          (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g))⁻¹) ↔
    x ∈ toConjAct g⁻¹ • Γ

Tactic:
← map_inv,

Goal state after:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ,
      toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) y) =
        toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) * toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) x) *
          toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)) ↔
    x ∈ toConjAct g⁻¹ • Γ
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
· simp [𝒢.relindex_adjoinNegOne_eq_two hG]

Goal state after:
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:
rw [SL_slash_apply, modular_S_smul]
  simp [ModularGroup.S, denom]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = (⇑normSq ∘ (fun p ↦ ↑(p 0) * ↑z + ↑(p 1)) ∘ fun p ↦ Int.cast ∘ p) x✝

Tactic:
dsimp only [Function.comp_def]

Goal state after:
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)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = normSq (↑↑(x✝ 0) * ↑z + ↑↑(x✝ 1))
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (fun x ↦ f (↑ofComplex x)) {z | 0 < z.im}
z : ℂ
h : z ∈ {z | 0 < z.im}
⊢ (fun x ↦ (starRingEnd ℂ) (f (↑ofComplex (-(starRingEnd ℂ) ↑(↑ofComplex x))))) z =
    (fun x ↦ (starRingEnd ℂ) (f (↑ofComplex (-(starRingEnd ℂ) x)))) z

Tactic:
simp [ofComplex_apply_of_im_pos h]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0»
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⁻¹ * g (f c) ((fun i ↦ i) ⟨0, ⋯⟩) = c ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
change (z : ℂ).im⁻¹ * (f c).im = c 0
      rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = -1 * f z
h2 : 2 * f z = 0
⊢ ¬2 = 0

Tactic:
by norm_num

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

Goal state before:
pp: case inl
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
hq : ‖0‖ < 1
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

pp: case inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
hq' : q ≠ 0
⊢ DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
· exact hfper.differentiableAt_cuspFunction_zero hh
      (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
        (fun z hz ↦ UpperHalfPlane.mdifferentiableAt_iff.mp (hfhol ⟨z, hz⟩)))
      (hfbdd.comp_tendsto tendsto_comap_im_ofComplex)

Goal state after:
case inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
hq' : q ≠ 0
⊢ DifferentiableAt ℂ (cuspFunction h f) q
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
⊢ Periodic (⇑f ∘ ↑ofComplex) ↑h

Tactic:
intro w
  by_cases! hw : 0 < im w
  · 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]
  · have : im (w + h) ≤ 0 := by simpa using hw
    simp [ofComplex_apply_of_im_nonpos this, ofComplex_apply_of_im_nonpos hw]

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

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ IsBoundedAtImInfty (⇑f ∣[k] g)

Tactic:
rw [← OnePoint.isBoundedAt_infty_iff, SL_slash, ← OnePoint.IsBoundedAt.smul_iff]
  apply bdd_at_cusps f
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']
  exact ⟨g, by simp [mapGL]⟩

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

Goal state before:
pp: k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ eisSummand k i (A • z) =
    denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) ↑z ^ k * eisSummand k (i ᵥ* ↑A) z

Tactic:
simp only [eisSummand, vecMul, vec2_dotProduct, denom, UpperHalfPlane.specialLinearGroup_apply]
  have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) : (u * ((a * z + b) / (c * z + d)) + v) ^ (-k) =
      (c * z + d) ^ k * ((u * a + v * c) * z + (u * b + v * d)) ^ (-k) := by
    replace hc : z * c + d ≠ 0 := by convert! hc using 1; ring
    field_simp
    simp [div_zpow]
    ring_nf
  simpa using h (hc := denom_ne_zero A z) ..

Goal state after: