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

Goal state before:
pp: a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
⊢ a = 2 ∧ Prime n

Tactic:
have hn0 : n ≠ 0 := fun h ↦ (h ▸ han1).ne' rfl

Goal state after:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
⊢ a = 2 ∧ Prime n
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
h : λ * λ ^ (3 * S.multiplicity - 2 + 1) * λ ∣ (λ ^ S.multiplicity * S.w) ^ 3
⊢ False

Tactic:
← pow_succ'

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (3 * S.multiplicity - 2 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * S.w) ^ 3
⊢ False
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₄ * S.Z ^ 3 = ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3

Tactic:
u₅_def,

Goal state after:
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₄ * S.Z ^ 3 = ↑(-η ^ 2 * S.u₁ * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
v : AbsoluteValue K ℝ
⊢ ⨆ i, v (Sum.elim x 0 i) = ⨆ i, v (x i)

Tactic:
exact H v

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

Goal state before:
pp: case h₂
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ 1 ≤ mulHeight A

pp: case h₂
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ 1 ≤ mulHeight x

Tactic:
· exact one_le_mulHeight _

Goal state after:
case h₂
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ 1 ≤ mulHeight x
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₂
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ 1 ≤ mulHeight x

Tactic:
· exact one_le_mulHeight _

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

Goal state before:
pp: case hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))

Tactic:
rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]
    simp_rw [mul_sub, mul_one]
    refine tendsto_const_nhds.sub (Tendsto.const_mul _ ?_)
    refine tendsto_const_nhds.div_atTop <| (tendsto_rpow_atTop (by linarith)).comp ?_
    exact tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop

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

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

Tactic:
grw [← le_max_left]

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

Goal state before:
pp: case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
hcd,

Goal state after:
case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight 0
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ![↑a, ↑n] ≠ 0

Tactic:
by simp [hn]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : mulHeight ![↑a, ↑n] ≤ B
⊢ ![↑a, ↑n] ≠ 0

Tactic:
by simp [hn]

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 : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
⊢ (h.algEquiv h') (h.map z) = h'.map z

Tactic:
rw [← h.algEquiv_map h']

Goal state after:
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
z : R[X]
⊢ (h.algEquiv h') (h.map z) = ((↑(h.algEquiv h')).comp h.map) z
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
a : 𝓞 K
ha : ↑n * x = ↑a
⊢ ∃ x_1, mulHeight ![↑x_1, ↑n] ≤ B ∧ ↑x_1 / ↑n = x

Tactic:
refine ⟨a, ?_, (EuclideanDomain.eq_div_of_mul_eq_right hn' ha).symm⟩

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
a : 𝓞 K
ha : ↑n * x = ↑a
⊢ mulHeight ![↑a, ↑n] ≤ B
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
a : 𝓞 K
ha : ↑n * x = ↑a
⊢ mulHeight ![↑a, ↑n] ≤ B

Tactic:
rwa [← ha, ← mulHeight₁_div_eq_mulHeight, mul_div_cancel_left₀ x hn']

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 : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z) - eval₂ i x w = 0

Tactic:
← eval₂_sub,

Goal state after:
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✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z - w) = 0
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
hf : 1 = v (∑ x_1, ↑(x x_1 * f x_1))
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
Int.cast_mul

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
hf : 1 = v (∑ x_1, ↑(x x_1) * ↑(f x_1))
⊢ ⨆ i, v ↑(x i) = 1
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 : R[X]
⊢ f ∣ h.repr (h.map g) - g

Tactic:
by rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]

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
hx₀ : Int.cast ∘ x ≠ 0
⊢ mulHeight (Int.cast ∘ x) = ↑(⨆ i, |x i|)

Tactic:
simp_rw [Finite.map_iSup_of_monotone _ Int.cast_mono, NumberField.mulHeight_eq hx₀,
    infinitePlace_apply]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
hx₀ : Int.cast ∘ x ≠ 0
⊢ (∏ x_1, (⨆ i, ↑|(Int.cast ∘ x) i|) ^ x_1.mult) * ∏ᶠ (v : FinitePlace ℚ), ⨆ i, v ((Int.cast ∘ x) i) = ⨆ i, ↑|x i|
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
⊢ ∃ C > 0,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]

Tactic:
refine ⟨C, hC₀, fun hab hcd ↦ ?_⟩

Goal state after:
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ C * mulHeight ![a✝, b✝] * mulHeight ![c✝, d✝] ≤ mulHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝]
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: q : ℚ
⊢ Finset.univ.gcd ![q.num, ↑q.den] = 1

Tactic:
simpa [Finset.univ_fin2, Int.normalize_coe_nat, ← Int.coe_gcd q.num q.den] using
      Int.isCoprime_iff_gcd_eq_one.mp <| isCoprime_num_den q

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

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

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
ih : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
hn₂ : n + 1 < orderOf χ
hχn : χ * χ ^ n ≠ 1
⊢ jacobiSum χ (χ ^ n) * gaussSum (χ * χ ^ n) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ

Tactic:
← pow_succ'

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
ih : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
hn₂ : n + 1 < orderOf χ
hχn : χ * χ ^ n ≠ 1
⊢ jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s ↦ Φ j * (↑N ^ (-s) * ((s - 1) * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j * (↑N ^ (-1) * 1)))

Tactic:
refine tendsto_const_nhds.mul (.mul ?_ <| hurwitzZeta_residue_one _)

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s ↦ ↑N ^ (-s)) (𝓝[≠] 1) (𝓝 (↑N ^ (-1)))
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : y = Ideal.map (algebraMap R S) I
⊢ y ∈ normalizedFactors (Ideal.map (algebraMap R S) I)

Tactic:
simp [hy]

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

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∀ᶠ (x : ℝ) in atTop, LSeries f ↑x = LSeries g ↑x
⊢ ∀ᶠ (x : ℝ) in atTop, LSeries (f - g) ↑x = 0 x

Tactic:
eventually_atTop

Goal state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ (b : ℝ), a ≤ b → LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → LSeries (f - g) ↑b = 0 b
Module: Mathlib.NumberTheory.LSeries.ZetaZeros

Goal state before:
pp: S : Set ℂ
hS : IsCompact S
⊢ (S ∩ riemannZetaZeros).Finite

Tactic:
apply (hS.inter_right isClosed_riemannZetaZeros).finite

Goal state after:
S : Set ℂ
hS : IsCompact S
⊢ IsDiscrete (S ∩ riemannZetaZeros)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
hp : p ≠ 2
ha0 : ↑a ≠ 0
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

Tactic:
by
  replace hp : Odd p := h.out.odd_of_ne_two hp
  have : (legendreSym p a : ZMod p) =
      (((-1) ^ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} : ℤ) : ZMod p) := by
    rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]
  cases legendreSym.eq_one_or_neg_one p ha0 <;>
  cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} <;>
  simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
⊢ ∃ x, 0 < ‖↑x‖ ∧ ‖↑x‖ < 1

Tactic:
obtain ⟨x, hx, hx'⟩ := NormedField.exists_norm_lt_one K

Goal state after:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : K
hx : 0 < ‖x‖
hx' : ‖x‖ < 1
⊢ ∃ x, 0 < ‖↑x‖ ∧ ‖↑x‖ < 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p' : ℕ
⊢ sZMod (p' + 2) 0 = ↑(s 0)

Tactic:
dsimp [s, sZMod]; simp

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: 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)
h_subset :
  {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B} ⊆
    {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}
h_finite : {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.Finite
⊢ {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite ∧
    {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤
      {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard

Tactic:
exact ⟨h_finite.subset h_subset, Set.ncard_le_ncard h_subset h_finite⟩

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

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
⊢ (f + g) ∣[k] A = f ∣[k] A + g ∣[k] A

Tactic:
ext1 τ
  simp [privateSlash, add_mul]

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

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
⊢ IsCusp (g • c) 𝒢

Tactic:
by
  convert! hc.smul g
  ext x
  rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← ConjAct.toConjAct_inv,
    ConjAct.toConjAct_smul, inv_inv, Subgroup.mul_mem_cancel_right _ hg,
    Subgroup.mul_mem_cancel_left _ (inv_mem hg)]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
this : GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ
⊢ f (h +ᵥ τ) =
    (σ (GeneralLinearGroup.upperRightHom h)) (f (h +ᵥ τ)) *
        ↑|↑(GeneralLinearGroup.det (GeneralLinearGroup.upperRightHom h))| ^ (k - 1) *
      denom (GeneralLinearGroup.upperRightHom h) ↑τ ^ (-k)

Tactic:
simp [σ, denom, GeneralLinearGroup.val_det_apply, denom]

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by cases f; cases g; congr; exact DFunLike.ext' h

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by cases f; cases g; congr; exact DFunLike.ext' h

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity✝ : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
hf_infinity : ∀ᶠ (b : ℝ) in atTop, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
eventually_atTop

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity✝ : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
hf_infinity : ∃ a, ∀ (b : ℝ), a ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|

Tactic:
obtain ⟨g, hg⟩ := Filter.Tendsto.exists_forall_le (tendsto_abs_re_smul z hcd)

Goal state after:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
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
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
x : ℝ
⊢ 0 < (↑x + 1 / ↑n * I).im

Tactic:
by simp [hn]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : ℤ → α
a : α
⊢ HasProd f a (symmetricIcc ℤ) ↔ Tendsto (fun N ↦ ∏ n ∈ Icc (-↑N) ↑N, f n) atTop (𝓝 a)

Tactic:
by
  simp [HasProd, symmetricIcc, ← Nat.map_cast_int_atTop, comp_def]

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

Goal state before:
pp: n : ℕ
z : ℂ
⊢ eta_q n z = cexp (2 * ↑π * I * z) ^ (n + 1)

Tactic:
simp [eta_q, Periodic.qParam]

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 : ‖↑z - 1‖ ≤ 1
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = 1 +ᵥ ρ

Tactic:
rw [norm_def, Real.sqrt_le_one] at hnorm

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 +ᵥ ρ