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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)

Goal state after:
case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

case neg
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)

Goal state after:
case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))

case neg
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
cases subsingleton_or_nontrivial R
  · have : Subsingleton Rₘ := Module.subsingleton R Rₘ
    simp [eq_iff_true_of_subsingleton]
  let b := Module.Free.chooseBasis R S
  let := Classical.decEq (Module.Free.ChooseBasisIndex R S)
  rw [Algebra.trace_eq_matrix_trace (b.localizationLocalization Rₘ M Sₘ),
    Algebra.trace_eq_matrix_trace b, ← Algebra.map_leftMulMatrix_localization]
  exact (AddMonoidHom.map_trace (algebraMap R Rₘ).toAddMonoidHom _).symm

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } ∈ unitary (ℤ√d)

Tactic:
rw [Unitary.mem_iff, isPell_norm, mul_comm (star _), and_self_iff]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ -x✝ + x✝ = 0

Tactic:
by ext; simp_rw [add_apply, neg_apply, neg_add_cancel, zero_apply]

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

Goal state before:
pp: d n : ℤ
⊢ ofInt n = ↑n

Tactic:
by ext <;> simp [re_ofInt, im_ofInt]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
have bm : (_ * ⟨_, _⟩ : ℤ√d a1) = 1 := Pell.isPell_norm.1 hp
        have y0l : (0 : ℤ√d a1) < ⟨x - x, y - -y⟩ :=
          sub_lt_sub h1l fun hn : (1 : ℤ√d a1) ≤ ⟨x, -y⟩ => by
            have t := mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)
            rw [bm, mul_one] at t
            exact h1l t
        have yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩ :=
          show (⟨x, y⟩ - ⟨x, -y⟩ : ℤ√d a1) < ⟨a, 1⟩ - ⟨a, -1⟩ from
            sub_lt_sub ha fun hn : (⟨x, -y⟩ : ℤ√d a1) ≤ ⟨a, -1⟩ => by
              have t := mul_le_mul_of_nonneg_right
                      (mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)) a1p
              rw [bm, one_mul, mul_assoc, Eq.trans (mul_comm _ _) a1m, mul_one] at t
              exact ha t
        simp only [sub_self, sub_neg_eq_add] at y0l; simp only [Zsqrtd.re_neg, add_neg_cancel,
          Zsqrtd.im_neg, neg_neg] at yl2
        exact
          match y, y0l, (yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩) with
          | 0, y0l, _ => y0l (le_refl 0)
          | (y + 1 : ℕ), _, yl2 =>
            yl2
              (Zsqrtd.le_of_le_le (by simp)
                (let t := Int.ofNat_le_ofNat_of_le (Nat.succ_pos y)
                add_le_add t t))
          | Int.negSucc _, y0l, _ => y0l trivial

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

Goal state before:
pp: d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : Int.natAbs 1 = x.norm.natAbs * y.norm.natAbs
⊢ x.norm.natAbs = 1

Tactic:
Int.natAbs_one,

Goal state after:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : 1 = x.norm.natAbs * y.norm.natAbs
⊢ x.norm.natAbs = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
⊢ b ≤ a ∨ a ≤ b

Tactic:
have t := (a - b).nonneg_total

Goal state after:
d : ℕ
a b : ℤ√↑d
t : (a - b).Nonneg ∨ (-(a - b)).Nonneg
⊢ b ≤ a ∨ a ≤ b
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
Nat.mod_eq_of_lt (strictMono_x _ lin)

Goal state after:
case refl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑k.toNat = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Tactic:
← hk

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < ↑k.toNat
hk₁ : ↑k.toNat ≤ ↑n
h : |↑↑k.toNat * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑k.toNat = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ ↑(xn a1 j % xn a1 n) < ↑(xn a1 (j + 1) % xn a1 n)

Tactic:
rw [lem2 j jn (le_of_lt j2n), lem2 (j + 1) (Nat.le_succ_of_le jn) j2n]

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ ↑(xn a1 n) - ↑(xn a1 (2 * n - j)) < ↑(xn a1 n) - ↑(xn a1 (2 * n - (j + 1)))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: ⊢ Dioph {v | ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3}

Tactic:
by
  have : Dioph {v : Vector3 ℕ 4 |
    1 < v &0 ∧ v &1 ≤ v &3 ∧
    (v &2 = 1 ∧ v &3 = 0 ∨
    ∃ u w s t b : ℕ,
      v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
      u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
      s * s - (b * b - 1) * t * t = 1 ∧
      1 < b ∧ b ≡ 1 [MOD 4 * v &3] ∧ b ≡ v &0 [MOD u] ∧
      0 < w ∧ v &3 * v &3 ∣ w ∧
      s ≡ v &2 [MOD u] ∧
      t ≡ v &1 [MOD 4 * v &3])} :=
  (D.1 D< D&0 D∧ D&1 D≤ D&3 D∧
    ((D&2 D= D.1 D∧ D&3 D= D.0) D∨
    ((D∃) 4 <| (D∃) 5 <| (D∃) 6 <| (D∃) 7 <| (D∃) 8 <|
    D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
    D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
    D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧
    D.1 D< D&0 D∧ (D≡ (D&0) (D.1) (D.4 D* D&8)) D∧ (D≡ (D&0) (D&5) (D&4)) D∧
    D.0 D< D&3 D∧ D&8 D* D&8 D∣ D&3 D∧
    (D≡ (D&2) (D&7) (D&4)) D∧
    (D≡ (D&1) (D&6) (D.4 D* (D&8))))) :)
  exact Dioph.ext this fun v => matiyasevic.symm

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inr.inr
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
⊢ n ^ k = m

Tactic:
have te : (t : ℤ) = 2 * xn hw1 j * n - n * n - 1 := by
      rw [sub_sub, eq_sub_iff_add_eq]
      exact mod_cast ta.symm

Goal state after:
case mpr.inr.inr
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
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ n ^ k = m
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x ↦ x ^ (-P.k)

Tactic:
← isBigO_norm_norm

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ ‖(P.ε * ↑(x ^ (-P.k))) • P.g₀‖) =O[𝓝[>] 0] fun x ↦ ‖x ^ (-P.k)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_3
t : ℝ
ht : 0 < t
⊢ F_nat 0 0 t - 1 = F_nat 0 1 t

Tactic:
rw [F_nat, (summable_f_nat 0 0 ht).tsum_eq_zero_add, f_nat, Nat.cast_zero, add_zero, pow_zero,
      one_mul, pow_two, mul_zero, mul_zero, zero_mul, exp_zero, add_comm, add_sub_cancel_right]

Goal state after:
case e'_3
t : ℝ
ht : 0 < t
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ (P.ε * ↑(x ^ P.k)) • P.g x - P.f₀ + 0 = (P.ε * ↑(x ^ P.k)) • (0 + (P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀))

Tactic:
simp_rw [rpow_neg hx.le]

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ (P.ε * ↑(x ^ P.k)) • P.g x - P.f₀ + 0 = (P.ε * ↑(x ^ P.k)) • (0 + (P.g x - (P.ε⁻¹ * ↑(x ^ P.k)⁻¹) • P.f₀))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) n) z τ

Tactic:
simp_rw [jacobiTheta₂_term, ← Complex.exp_add, Equiv.coe_addRight, Int.cast_add]

Goal state after:
z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    cexp (-↑π * I * (τ + 2 * z) + (2 * ↑π * I * (↑n + ↑1) * z + ↑π * I * (↑n + ↑1) ^ 2 * τ))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case pos
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 1)

pp: case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Tactic:
· obtain ⟨k, rfl⟩ := h
    simpa [← Int.cast_add, add_eq_zero_iff_eq_neg]
      using hasSum_ite_sub_hasSum (hasSum_int_evenKernel (k : ℝ) ht) (-k)

Goal state after:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s

Tactic:
by
  rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedCosZeta a (1 - s) = completedHurwitzZetaEven a s

Tactic:
by
  rw [← completedHurwitzZetaEven_one_sub, sub_sub_cancel]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
hn : n ≠ 0
⊢ 1 n = ↑((fun x ↦ ζ x) n)

Tactic:
by
  simp [hn]

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

Goal state before:
pp: case inr.inl
χ : DirichletCharacter ℂ 0
hn : 1 ≠ 0
⊢ χ ↑1 = δ 1

Tactic:
simp [delta]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s)

Tactic:
let c (n : ℤ) : ℂ := cexp (2 * π * I * a * n) / 2
  have hF t (ht : 0 < t) : HasSum (fun n : ℤ ↦ if n = 0 then 0 else c n * rexp (-π * n ^ 2 * t))
      ((cosKernel a t - 1) / 2) := by
    refine ((hasSum_int_cosKernel₀ a ht).div_const 2).congr_fun fun n ↦ ?_
    split_ifs <;> simp [c, div_mul_eq_mul_div]
  simp only [← Int.cast_eq_zero (α := ℝ)] at hF
  rw [show completedCosZeta a s = mellin (fun t ↦ (cosKernel a t - 1 : ℂ) / 2) (s / 2) by
    rw [mellin_div_const, completedCosZeta]
    congr 1
    refine ((hurwitzEvenFEPair a).symm.hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
    rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]]
  refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
  · apply (((summable_one_div_int_add_rpow 0 s.re).mpr hs).div_const 2).of_norm_bounded
    intro i
    simp only [c, (by { push_cast; ring } : 2 * π * I * a * i = ↑(2 * π * a * i) * I), norm_div,
      RCLike.norm_ofNat, Complex.norm_exp_ofReal_mul_I, add_zero, norm_one,
      norm_of_nonneg (by positivity : 0 ≤ |(i : ℝ)| ^ s.re), div_right_comm, le_rfl]
  · simp [c, ← Int.cast_abs, div_right_comm, mul_div_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremWith R m
⊢ FermatLastTheoremWith R n

Tactic:
rintro a b c ha hb hc
  obtain ⟨k, rfl⟩ := hmn
  simp_rw [pow_mul']
  refine hm _ _ _ ?_ ?_ ?_ <;> exact pow_ne_zero _ ‹_›

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
⊢ h.IsPrimitiveClassified

Tactic:
rcases Int.natAbs_eq y with hy | hy

Goal state after:
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ h.IsPrimitiveClassified

case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ h.IsPrimitiveClassified
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha₀ : a ≠ 0
⊢ (normalizedFactors a).Nodup

Tactic:
rwa [← squarefree_iff_nodup_normalizedFactors ha₀, ← isRadical_iff_squarefree_of_ne_zero ha₀]

Goal state after:
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
⊢ ↑(Ideal.absNorm (num 0)) / ↑|(Algebra.norm ℤ) ↑(den 0)| = 0

Tactic:
rw [num_zero_eq, Submodule.zero_eq_bot, Ideal.absNorm_bot, Nat.cast_zero, zero_div]

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
⊢ Function.Injective ⇑(algebraMap R K)
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: x : 𝓞 ℚ
⊢ x = 1 ∨ x = -1 ↔ ↑x = 1 ∨ ↑x = -1

Tactic:
←
    Subtype.coe_injective.eq_iff

Goal state after:
x : 𝓞 ℚ
⊢ ↑x = ↑1 ∨ ↑x = ↑(-1) ↔ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
⊢ w = v ↔ (↑w).IsEquiv ↑v

Tactic:
refine ⟨fun h ↦ h ▸ .rfl, fun h ↦ ?_⟩
  obtain ⟨t, _, h⟩ := w.1.isEquiv_iff_exists_rpow_eq.1 h
  exact ext _ _ fun k ↦ by simpa [eq_one_of_rpow_eq h, ext, coe_apply] using funext_iff.1 h k

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ nrComplexPlaces K = 0 ↔ IsTotallyReal K

Tactic:
by
  simp [Fintype.card_eq_zero_iff, isEmpty_subtype, isTotallyReal_iff]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (mixedSpace K) = finrank ℚ K

Tactic:
rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
    card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul,
    mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
    Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))

Tactic:
exact ⟨by rcases embedding_mk_eq φ with (_ | _) <;> aesop, h.1⟩

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x + y).1 ⟨w, hw⟩‖ else ‖(x + y).2 ⟨w, ⋯⟩‖) ≤
    (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) + if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs <;> exact norm_add_le _ _

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ 0 ≤ ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x

Tactic:
exact Finset.sum_nonneg (fun _ _ => mul_nonneg (Nat.cast_pos.mpr mult_pos).le
      (normAtPlace_nonneg _ _))

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ
⊢ ‖x‖₊ = (image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ).sup fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯

Tactic:
sup_union,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ
⊢ ‖x‖₊ =
    max ((image (fun w ↦ ↑w) univ).sup fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯)
      ((image (fun w ↦ ↑w) univ).sup fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ
⊢ ‖x‖₊ = univ.sup fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯

Tactic:
rw [this, sup_union, univ.sup_image, univ.sup_image,
    Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ
⊢ max (univ.sup fun b ↦ ‖x.1 b‖₊) (univ.sup fun b ↦ ‖x.2 b‖₊) =
    max (univ.sup ((fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) ∘ fun w ↦ ↑w))
      (univ.sup ((fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) ∘ fun w ↦ ↑w))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
x✝ : Gal(K/k)
⊢ x✝ = 1 ∨ ComplexEmbedding.IsConj φ x✝ ↔ x✝ ∈ {1, σ}

Tactic:
Set.mem_insert_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
x✝ : Gal(K/k)
⊢ x✝ = 1 ∨ ComplexEmbedding.IsConj φ x✝ ↔ x✝ = 1 ∨ x✝ ∈ {σ}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (fromBlocks (diagonal fun x ↦ 1) 0 0
        ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
          (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]))).det =
    ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det

Tactic:
det_fromBlocks_zero₂₁,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (diagonal fun x ↦ 1).det *
      ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
          (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I])).det =
    ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    (fromBlocks (diagonal fun x ↦ 1) 0 0
          ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
            (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I])) *ᵥ
        x ∘ ⇑(indexEquiv K))
      c

Tactic:
mulVec,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    (fun j ↦
        fromBlocks (diagonal fun x ↦ 1) 0 0
          ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
            (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]))
          c j) ⬝ᵥ
      x ∘ ⇑(indexEquiv K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (ZSpan.fundamentalDomain (stdBasis K)) = 1

Tactic:
volume_fundamentalDomain_stdBasis K

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 1 = 1