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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
⊢ Ideal.span {(algebraMap R S) M} * ↑I ≤ Ideal.span {b}

Tactic:
Ideal.mul_le

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
⊢ ∀ r ∈ Ideal.span {(algebraMap R S) M}, ∀ s ∈ ↑I, r * s ∈ Ideal.span {b}
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)

Tactic:
by
  simpa using rootsOfUnity.integer_power_of_ringEquiv n g

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ 1 < x → log x ^ 2 ≠ 0

Tactic:
_

Goal state after:
x : ℝ
a✝ : 1 < x
⊢ log x ^ 2 ≠ 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ 4 ≤ x → ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ log 4 * ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖

Tactic:
_

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ log 4 * ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast

Tactic:
simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]
      rw [mul_comm, unitCoeff_spec h] at hc
      suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec
      lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
      rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
      exact irreducible_p

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ 0 < x → (log x)⁻¹ = x / log x ^ 2 / (x / log x)

Tactic:
_

Goal state after:
x : ℝ
a✝ : 0 < x
⊢ (log x)⁻¹ = x / log x ^ 2 / (x / log x)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (toZModPow n) ((lift f_compat) r) = (toZModPow n) ↑((f n) r).val

Tactic:
←
    sub_eq_zero,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (toZModPow n) ((lift f_compat) r) - (toZModPow n) ↑((f n) r).val = 0
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
rw [discr_powerBasis_eq_norm, finrank L hirr, hζ.powerBasis_gen _,
    ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, totient_prime_pow hp.out (succ_pos k),
    Nat.add_one_sub_one]

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) *
      (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) =
    (-1) ^ (p ^ k * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
⊢ (toZModPow n) x = ↑(f n)

Tactic:
have hs : x = Padic.mk s := rfl

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
⊢ (toZModPow n) x = ↑(f n)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ 1 ≤ b * { re := ↑a, im := -1 }

Tactic:
rw [← a1m]; exact mul_le_mul_of_nonneg_right ha am1p

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ * 1) x✝ = x✝¹ x✝

Tactic:
rw [mul_apply, one_apply, mul_one]

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

Goal state before:
pp: c d : ℕ
x y : ℤ
⊢ Nonnegg c d x y = Nonnegg d c y x

Tactic:
cases x <;> cases y <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ x) ⊗ t) s

Tactic:
rcases s with a | b <;> try { cases a <;> rfl }

Goal state after:
case inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) s

Tactic:
rcases s with a | b <;> try { cases a <;> rfl }

Goal state after:
case inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
b : γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inr b)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
s : Option α ⊕ β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (t none ::ₒ v ⊗ t ∘ some) s

Tactic:
rcases s with a | b <;> try { cases a <;> rfl }

Goal state after:
case inr
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
| HasSum (fun x ↦ f ↑((equivProdNatFactoredNumbers hpp hp) x))
    ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n))

Tactic:
1,

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
| fun x ↦ f ↑((equivProdNatFactoredNumbers hpp hp) x)
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
| ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε

Tactic:
1,

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
| fun N₀ ↦ ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
⊢ ↑t + (↑n * ↑n + 1) = 2 * ↑(xn hw1 j) * ↑n

Tactic:
exact mod_cast ta.symm

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

Goal state before:
pp: case isFalse.zero
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
⊢ 0 ≤ logMul^[0] a k

Tactic:
simpa only [Function.iterate_zero, id_eq] using! hn k

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
k : ℕ
| Tendsto (fun x ↦ -(-π * (T * ↑x ^ 2 - 2 * S * ↑x) - -1 * ↑x)) atTop atTop

Tactic:
1,

Goal state after:
S T : ℝ
hT : 0 < T
k : ℕ
| fun x ↦ -(-π * (T * ↑x ^ 2 - 2 * S * ↑x) - -1 * ↑x)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(x ^ (r + P.k))⁻¹⁻¹‖ / (‖P.ε⁻¹‖ * ‖x ^ P.k‖)

Tactic:
inv_inv,

Goal state after:
case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖x ^ (r + P.k)‖ / (‖P.ε⁻¹‖ * ‖x ^ P.k‖)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
| Tendsto (fun n ↦ rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)) atTop atTop

Tactic:
1,

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
| fun n ↦ rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ Summable fun i ↦ ‖a i‖ / (π * q i) ^ s.re

Tactic:
have (i : _) : ‖a i‖ / ↑(π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re := by
      rcases hq i with h | h
      · simp [h]
      · rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
this : ∀ (i : ι), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ Summable fun i ↦ ‖a i‖ / (π * q i) ^ s.re
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
have (i t : _) : (if p i = 0 then 0 else a i * rexp (-π * p i * t)) =
      a' i * rexp (-π * p i * t) := by
    simp [a']

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case H
a' : ℝ
⊢ ContinuousOn (fun x ↦ jacobiTheta₂ (↑a') (I * ↑x)) (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)

Goal state after:
case H
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ jacobiTheta₂ (↑a') (I * ↑x)) x
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
t : ℝ
ht : t ∈ Ioi 0
| HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)

Tactic:
1,

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
t : ℝ
ht : t ∈ Ioi 0
| fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂ z τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
rw [← jacobiTheta₂_neg_left, jacobiTheta₂, conj_tsum]
  congr 2 with n
  simp only [jacobiTheta₂_term, mul_neg, ← exp_conj, map_add, map_neg, map_mul, map_ofNat,
    conj_ofReal, conj_I, map_intCast, neg_mul, neg_neg, map_pow]

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

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ Function.Periodic (fun a ↦ (jacobiTheta₂'' (↑a) (I * ↑x)).re) 1

Tactic:
simp [jacobiTheta₂''_add_left]

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

Goal state before:
pp: s : ℂ
⊢ False ∨ sinZeta 0 s = 0

Tactic:
false_or,

Goal state after:
s : ℂ
⊢ sinZeta 0 s = 0
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: case pos
h : LSeriesSummable (fun n ↦ ↑(μ n)) 1
n : ℕ
hn : Nat.Prime n
⊢ {n | Nat.Prime n}.indicator (term (fun n ↦ ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n ↦ 1 / ↑n) n)

pp: case neg
h : LSeriesSummable (fun n ↦ ↑(μ n)) 1
n : ℕ
hn : ¬Nat.Prime n
⊢ {n | Nat.Prime n}.indicator (term (fun n ↦ ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n ↦ 1 / ↑n) n)

Tactic:
· simp [hn, hn.ne_zero, moebius_apply_prime hn, push_cast, neg_div]

Goal state after:
case neg
h : LSeriesSummable (fun n ↦ ↑(μ n)) 1
n : ℕ
hn : ¬Nat.Prime n
⊢ {n | Nat.Prime n}.indicator (term (fun n ↦ ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n ↦ 1 / ↑n) n)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ 2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) (sinKernel (↑a) t)

Tactic:
by
  rw [← hasSum_ofReal]
  have := (hasSum_int_sinKernel a ht).nat_add_neg
  simp only [Int.cast_zero, zero_mul, mul_zero, add_zero] at this
  refine this.congr_fun fun n ↦ ?_
  simp_rw [Int.cast_neg, neg_sq, mul_neg, ofReal_mul, Int.cast_natCast, ofReal_natCast,
      ofReal_ofNat, ← add_mul, ofReal_sin, Complex.sin]
  push_cast
  congr 1
  rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self two_ne_zero, one_mul,
    neg_mul, neg_mul, neg_neg, mul_comm _ I, ← mul_assoc, mul_comm _ I, neg_mul,
    ← sub_eq_neg_add, mul_sub]
  congr 3 <;> ring

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False

Tactic:
rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n a✝ : ℕ
⊢ ∀ (b c : ℕ), a✝ = 1 → b = 1 → c = 1 → a✝ ^ n + b ^ n ≠ c ^ n

Tactic:
_

Goal state after:
n a✝ b✝ : ℕ
⊢ ∀ (c : ℕ), a✝ = 1 → b✝ = 1 → c = 1 → a✝ ^ n + b✝ ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n a✝ b✝ : ℕ
⊢ ∀ (c : ℕ), a✝ = 1 → b✝ = 1 → c = 1 → a✝ ^ n + b✝ ^ n ≠ c ^ n

Tactic:
_

Goal state after:
n a✝ b✝ c✝ : ℕ
⊢ a✝ = 1 → b✝ = 1 → c✝ = 1 → a✝ ^ n + b✝ ^ n ≠ c✝ ^ n
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z : ZMod 4
⊢ z * z ≠ 2

Tactic:
by
  change Fin 4 at z
  fin_cases z <;> decide

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
⊢ (primeFactors a).val = normalizedFactors a

Tactic:
rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
  exact normalizedFactors_nodup ha

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
by
  rcases hmn with h1 | h2
  · exact coprime_sq_sub_mul_of_even_odd h h1.left h1.right
  · exact coprime_sq_sub_mul_of_odd_even h h2.left h2.right

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

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ c ≠ 0 → a ^ 4 + b ^ 4 ≠ c ^ 4

Tactic:
_

Goal state after:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
⊢ a ^ 4 + b ^ 4 ≠ c ^ 4
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case pos
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
rw [hw] at wab wbc

Goal state after:
case pos
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case cons
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih : (↑s).Pairwise (Function.onFun IsRelPrime f) → radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i)
h : (↑(Finset.cons i s his)).Pairwise (Function.onFun IsRelPrime f)
⊢ radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)

Tactic:
Finset.coe_cons,

Goal state after:
case cons
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih : (↑s).Pairwise (Function.onFun IsRelPrime f) → radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i)
h : (insert i ↑s).Pairwise (Function.onFun IsRelPrime f)
⊢ radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
⊢ radical (a * b) ∣ radical a * radical b

Tactic:
by
  classical
  obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]

Goal state after: