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
a : S
b : R
hb : b ≠ 0
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
by
  have dim_pos := Fintype.card_pos_iff.mpr bS.index_nonempty
  set ε : ℝ := normBound abv bS ^ (-1 / Fintype.card ι : ℝ) with ε_eq
  have hε : 0 < ε := Real.rpow_pos_of_pos (Int.cast_pos.mpr (normBound_pos abv bS)) _
  have ε_le : (normBound abv bS : ℝ) * (abv b • ε) ^ (Fintype.card ι : ℝ)
                ≤ abv b ^ (Fintype.card ι : ℝ) := by
    have := normBound_pos abv bS
    have := abv.nonneg b
    rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one,
      mul_left_comm, mul_inv_cancel₀, mul_one, rpow_natCast] <;>
      try norm_cast; lia
    · exact Int.cast_nonneg this
    · linarith
  set μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
  let s : ι →₀ R := bS.repr a
  have s_eq : ∀ i, s i = bS.repr a i := fun i => rfl
  let qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b
  let rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b
  have r_eq : ∀ j i, rs j i = μ j * s i % b := fun i j => rfl
  have μ_eq : ∀ i j, μ j * s i = b * qs j i + rs j i := by
    intro i j
    rw [r_eq, EuclideanDomain.div_add_mod]
  have μ_mul_a_eq : ∀ j, μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i := by
    intro j
    rw [← bS.sum_repr a]
    simp only [μ, qs, rs, Finset.smul_sum, ← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [← s_eq, ← mul_smul, μ_eq, add_smul, mul_smul, ← μ_eq]
  obtain ⟨j, k, j_ne_k, hjk⟩ := adm.exists_approx hε hb fun j i => μ j * s i
  have hjk' : ∀ i, (abv (rs k i - rs j i) : ℝ) < abv b • ε := by simpa only [r_eq] using hjk
  let q := ∑ i, (qs k i - qs j i) • bS i
  set r := μ k - μ j with r_eq
  refine ⟨q, r, (mem_finsetApprox bS adm).mpr ?_, ?_⟩
  · exact ⟨k, j, j_ne_k.symm, rfl⟩
  have : r • a - b • q = ∑ x : ι, (rs k x • bS x - rs j x • bS x) := by
    simp only [q, r_eq, sub_smul, μ_mul_a_eq, Finset.smul_sum, ← Finset.sum_add_distrib,
      ← Finset.sum_sub_distrib, smul_sub]
    refine Finset.sum_congr rfl fun x _ => ?_
    ring
  rw [this, Algebra.norm_algebraMap_of_basis bS, abv.map_pow]
  refine Int.cast_lt.mp ((norm_lt abv bS _ fun i => lt_of_le_of_lt ?_ (hjk' i)).trans_le ?_)
  · apply le_of_eq
    congr
    simp_rw [map_sum, map_sub, map_smul, Finset.sum_apply',
      Finsupp.sub_apply, Finsupp.smul_apply, Finset.sum_sub_distrib, Basis.repr_self_apply,
      smul_eq_mul, mul_boole, Finset.sum_ite_eq', Finset.mem_univ, if_true]
  · exact mod_cast ε_le

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ IntegrableOn (fun t ↦ θ t / (t * log t ^ 2)) (Set.Icc 2 x) volume

Tactic:
by
  conv => arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]
  refine integrableOn_mul_sum_Icc _ (by norm_num) <| ContinuousOn.integrableOn_Icc fun x hx ↦
    ContinuousAt.continuousWithinAt ?_
  have : x ≠ 0 := by linarith [hx.1]
  have : x * log x ^ 2 ≠ 0 := mul_ne_zero this <| by simp; grind
  fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
⊢ ↑p ∣ x

Tactic:
← norm_lt_one_iff_dvd,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : x.zmodRepr = 0
⊢ ‖x‖ < 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

Tactic:
intro z ⟨_, _⟩

Goal state after:
case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
⊢ DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) z
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n

pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : ¬x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n + p ^ n * (toZMod (↑(unitCoeff h✝) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val

Tactic:
· rfl

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : ¬x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n + p ^ n * (toZMod (↑(unitCoeff h✝) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
b : ℤ√↑(d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ ↑n ≤ pellZd a1 n

Tactic:
by
      rw [Zsqrtd.natCast_val]
      exact
        Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _)
          (Int.natCast_nonneg _)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 m < xn a1 n * a + d a1 * yn a1 n

Tactic:
refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 n < xn a1 n * a
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Tactic:
let t := le_antisymm xy yx
    rw [one_mul] at t
    exact absurd t (not_divides_sq _ _)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : (q fun x ↦ (v ⊗ t) ((inl ⊗ fun x ↦ inr (inr x)) x)) = 0
⊢ q (v ⊗ t ∘ inr) = 0

Tactic:
rwa [show
                    (fun x : α ⊕ γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) =
                      v ⊗ t ∘ inr
                    from funext fun s => by rcases s with a | b <;> rfl] at hq

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
⊢ ∃ χ, χ a ≠ 1

Tactic:
by_cases hu : IsUnit a
  · refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_
    refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_
    contrapose ha
    rw [← hu.unit_spec, ha, Units.val_eq_one]
  · exact ⟨1, by simpa only [map_nonunit _ hu] using zero_ne_one⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False

Tactic:
rw [n1, i2] at hin; exact absurd hin (by decide)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 1 ≡ xn b1 1 [MOD c] ∧ yn a1 1 ≡ yn b1 1 [MOD c]

Tactic:
simpa [Nat.ModEq.refl]

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
⊢ ∑ χ, χ a = 0

Tactic:
obtain ⟨χ, hχ⟩ := exists_apply_ne_one_of_hasEnoughRootsOfUnity R ha

Goal state after:
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ χ, χ a = 0
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u ≤ ξ ∧ ξ < ↑u + 1

Tactic:
convert! And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2)

Goal state after:
case e'_5
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u = ↑u / ↑↑1

case e'_6
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ 1 = (↑↑1 * (2 * ↑↑1 - 1))⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ = 2 * π * ↑|n|

Tactic:
simp only [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
    norm_intCast, mul_one, Int.cast_abs]

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Tactic:
filter_upwards [eventually_le_nhds zero_lt_one] with x hx' (hx : 0 < x)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ *
      ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (3 * π * ↑|n| ^ 2)

Tactic:
(by norm_num : (3 : ℝ) = 2 + 1),

Goal state after:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ *
      ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * ((2 + 1) * π * ↑|n| ^ 2)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume
⊢ IntegrableAtFilter ((Ioo 0 1).indicator fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (𝓝[Ioi 0] x) volume

Tactic:
exact ⟨s, hs, hs'.indicator measurableSet_Ioo⟩

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

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

Tactic:
Nat.cast_ofNat,

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

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

Tactic:
convert! h_sum using 3 with i
    rw [← sq_abs, ← rpow_natCast_mul (abs_nonneg _), div_ofNat_re, Nat.cast_ofNat,
      mul_div_cancel₀ _ two_pos.ne']

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] ↑P.k) (𝓝 (-P.ε • P.g₀))

Tactic:
refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_
    filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ P.k)
    match_scalars
    grind

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

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ cexp (2 * (↑π * (I * (-↑n * -z))) + ↑π * (I * (↑n ^ 2 * τ))) =
    cexp (2 * (↑π * (I * (↑n * z))) + ↑π * (I * (↑n ^ 2 * τ)))

Tactic:
neg_mul_neg

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

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I * cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * ↑π *
        (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
          (jacobiTheta₂' (z * (-1 / τ)) (-1 / τ) + z * jacobiTheta₂ (z * (-1 / τ)) (-1 / τ) * (2 * ↑π * I))) /
      (2 * ↑π * I)

Tactic:
← div_mul_eq_mul_div (-2 * π : ℂ),

Goal state after:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I * cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * ↑π / (2 * ↑π * I) *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (jacobiTheta₂' (z * (-1 / τ)) (-1 / τ) + z * jacobiTheta₂ (z * (-1 / τ)) (-1 / τ) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ ∑' (n : ℤ), cexp (-↑π * (-I * τ) * ↑n ^ 2 + 2 * ↑π * (I * z) * ↑n) =
    1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2)

Tactic:
rw [tsum_exp_neg_quadratic h2]

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

Goal state before:
pp: case neg
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
h : ¬n = 0
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

Tactic:
· rfl

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

Goal state before:
pp: case hf
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
n : ℤ
⊢ (fun n ↦ (↑n ^ k)⁻¹) (-n) = (fun n ↦ (↑n ^ k)⁻¹) n

Tactic:
simp [Even.neg_pow hk2]

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: r : ℝ
⊢ (Summable fun p ↦ ↑↑p ^ r) ↔ r < -1

Tactic:
by_cases h : r < -1
  · -- case `r < -1`
    simp only [h, iff_true]
    exact (Real.summable_nat_rpow.mpr h).subtype _
  · -- case `-1 ≤ r`
    simp only [h, iff_false]
    refine fun H ↦ Nat.Primes.not_summable_one_div <| H.of_nonneg_of_le (fun _ ↦ by positivity) ?_
    intro p
    rw [one_div, ← Real.rpow_neg_one]
    exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast p.prop.one_lt.le) <| not_lt.mp h

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ h.IsPrimitiveClassified

Tactic:
use 0, 1

Goal state after:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ (0 = 0 ^ 2 - 1 ^ 2 ∧ y = 2 * 0 * 1 ∨ 0 = 2 * 0 * 1 ∧ y = 0 ^ 2 - 1 ^ 2) ∧
    Int.gcd 0 1 = 1 ∧ (0 % 2 = 0 ∧ 1 % 2 = 1 ∨ 0 % 2 = 1 ∧ 1 % 2 = 0)
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ wronskian 0 a = 0

Tactic:
← wronskianBilin_apply 0 a,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ ((wronskianBilin R) 0) a = 0
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
h : a = 0
⊢ False

Tactic:
subst h

Goal state after:
R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : wronskian 0 b ≠ 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
h : b = 0
⊢ False

Tactic:
subst h

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R[X]
ha : a ≠ 0
hw : a.wronskian 0 ≠ 0
⊢ False
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
ha' : a ≠ 0
⊢ Associated (radical a) a

Tactic:
rw [radical, ← Finset.prod_val, primeFactors_val_eq_normalizedFactors ha]

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha' : a ≠ 0
⊢ Associated (normalizedFactors a).prod a
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ w.natDegree < a.natDegree + b.natDegree

Tactic:
rw [wab] at hw ⊢

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : a.wronskian b ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd' : ¬r * s = -d ^ 2
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
hic : i.natAbs < c.natAbs
⊢ False

Tactic:
have hic' : Int.natAbs c ≤ Int.natAbs i := by
    apply h.2 j k i
    exact ⟨hj0, hk0, hh.symm⟩

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd' : ¬r * s = -d ^ 2
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
hic : i.natAbs < c.natAbs
hic' : c.natAbs ≤ i.natAbs
⊢ False
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: 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 : w = a.wronskian b
hbc : IsCoprime b c
⊢ b + c + a = 0

Tactic:
rwa [add_rotate] at hsum

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

Goal state before:
pp: case inr.refine_1.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
x✝ : ∃ n, a ∣ b ^ n
n : ℕ
hdvd : a ∣ b ^ n
hn : n ≠ 0
⊢ radical b ∣ b

Tactic:
radical_dvd_self

Goal state after:
case inr.refine_1.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
x✝ : ∃ n, a ∣ b ^ n
n : ℕ
hdvd : a ∣ b ^ n
hn : n ≠ 0
⊢ b ∣ b
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} * I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
simp_rw [← Nat.cast_natAbs, ← Nat.cast_mul, ← Ideal.absNorm_span_singleton]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} * I.num
⊢ ↑(Ideal.absNorm I.num * Ideal.absNorm (Ideal.span {↑a})) = ↑(Ideal.absNorm I₀ * Ideal.absNorm (Ideal.span {↑I.den}))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ h.IsClassified

Tactic:
apply h.isClassified_of_normalize_isPrimitiveClassified

Goal state after:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ⋯.IsPrimitiveClassified
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ⋯.IsPrimitiveClassified

Tactic:
apply h.normalize.isPrimitiveClassified_of_coprime

Goal state after:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ (x / ↑(x.gcd y)).gcd (y / ↑(x.gcd y)) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
· exfalso
        revert h_pos
        rw [h_neg]
        exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))

Goal state after: