mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp : ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ #univ • r ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
rw [nsmul_eq_mul]

Goal state after:
case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp : ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ ↑(#univ) * r ≤ ↑(Fintype.card (InfinitePlace K)) * r
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
have : p.map (algebraMap A B) ∣ a ^ e := by
    obtain ⟨b, hb⟩ := hP
    apply_fun (· ^ e : Ideal B → _) at ha
    apply_fun (· ^ (e - 1) : Ideal B → _) at hb
    simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
    conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
    rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha
    exact ⟨_, ha.symm⟩

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (algebraMap A B) p ∣ a ^ e
⊢ P ^ (e - 1) ∣ differentIdeal A B
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case inr
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
rw [if_neg (Nat.not_even_iff_odd.mpr hn)]
    have := (Nat.eq_or_eq_of_totient_eq_totient (Nat.dvd_lcm_left _ _) h_main).resolve_left ?_
    · rw [this, eq_comm, Nat.lcm_eq_right_iff_dvd]
      exact dvd_torsionOrder_of_isPrimitiveRoot hζ
    · rw [eq_comm, Nat.lcm_eq_left_iff_dvd]
      exact fun h ↦ Nat.not_even_iff_odd.mpr (Odd.of_dvd_nat hn h) (even_torsionOrder K)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ (logEmbedding K) (Additive.ofMul (fundSystem K i)) = ↑((basisUnitLattice K) i)

Tactic:
by
  rw [basisUnitLattice, Basis.map_apply, ← fundSystem_mk, logEmbeddingEquiv_apply]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑(∑ i ∈ m.divisors, i) * ↑k ≤ ↑(∑ i ∈ (m * k).divisors, i)

Tactic:
← cast_mul,

Goal state after:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑((∑ i ∈ m.divisors, i) * k) ≤ ↑(∑ i ∈ (m * k).divisors, i)
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑(#{x | x ^ 2 = a}.toFinset) = (quadraticChar F) a + 1

Tactic:
by
  -- we consider the cases `a = 0`, `a` is a nonzero square and `a` is a nonsquare in turn
  by_cases h₀ : a = 0
  · simp only [h₀, sq_eq_zero_iff, Set.ofPred_eq_eq_singleton, Set.toFinset_card,
    Set.card_singleton, Int.natCast_succ, Int.ofNat_zero, MulChar.map_zero]
  · set s := {x : F | x ^ 2 = a}.toFinset
    by_cases h : IsSquare a
    · rw [(quadraticChar_one_iff_isSquare h₀).mpr h]
      rcases h with ⟨b, h⟩
      rw [h, mul_self_eq_zero] at h₀
      have h₁ : s = [b, -b].toFinset := by
        ext1
        rw [← pow_two] at h
        simp_rw [s, Set.toFinset_ofPred, mem_filter_univ, h, List.toFinset_cons, List.toFinset_nil,
          insert_empty_eq, mem_insert, mem_singleton]
        exact sq_eq_sq_iff_eq_or_eq_neg
      norm_cast
      rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]
      exact card_pair (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))
    · rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]
      simp only [neg_add_cancel, Int.natCast_eq_zero, card_eq_zero, eq_empty_iff_forall_notMem]
      simpa [s, isSquare_iff_exists_sq, eq_comm] using h

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ ∃ S₁, S₁.isMinimal

Tactic:
by
  classical
  let T := {n | ∃ (S' : Solution hζ), S'.multiplicity = n}
  rcases Nat.find_spec (⟨S.multiplicity, ⟨S, rfl⟩⟩ : T.Nonempty) with ⟨S₁, hS₁⟩
  exact ⟨S₁, fun S'' ↦ hS₁ ▸ Nat.find_min' _ ⟨S'', rfl⟩⟩

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
inst✝⁹ : IsDomain A
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : Module.Finite A B
inst✝⁴ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝³ : p.IsMaximal
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
⊢ ¬P ∣ differentIdeal A B

Tactic:
by
  let : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap (by
      rw [← Ideal.map_le_iff_le_comap, ← hP]
      exact Ideal.mul_le_right)
  have : IsScalarTower A (A ⧸ p) (B ⧸ Q) := .of_algebraMap_eq' rfl
  have : Module.Finite (A ⧸ p) (B ⧸ Q) :=
    Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ Q)
  let e : (B ⧸ p.map (algebraMap A B)) ≃ₐ[A ⧸ p] ((B ⧸ P) × B ⧸ Q) :=
    { __ := (Ideal.quotEquivOfEq hP.symm).trans (Ideal.quotientMulEquivQuotientProd P Q hPQ),
      commutes' := Quotient.ind fun _ ↦ rfl }
  obtain ⟨x, hx⟩ : ∃ x, Algebra.trace (A ⧸ p) (B ⧸ P) x ≠ 0 := by
    simpa [LinearMap.ext_iff] using Algebra.trace_ne_zero (A ⧸ p) (B ⧸ P)
  obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (e.symm (x, 0))
  refine not_dvd_differentIdeal_of_intTrace_not_mem A P Q hP y ?_ ?_
  · have := congr((e $hy).2)
    simp at this
    simpa [e, Ideal.Quotient.eq_zero_iff_mem] using this
  · rw [← Ideal.Quotient.eq_zero_iff_mem, ← Algebra.trace_quotient_eq_of_isDedekindDomain,
      hy, Algebra.trace_eq_of_algEquiv, Algebra.trace_prod_apply]
    simpa

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ differentIdeal A B ≤ P

Tactic:
differentialIdeal_le_iff (K := K) (L := L) hPbot,

Goal state after:
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑(↑P)⁻¹) ≤ 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ P ∣ differentIdeal A B

Tactic:
rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) hPbot, hP,
      Submodule.map_le_iff_le_comap]

Goal state after:
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ Submodule.restrictScalars A ↑(↑a / ↑(Ideal.map (algebraMap A B) p)) ≤ comap (↑A (Algebra.trace K L)) 1
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: n : ℕ
s : Set ℕ
⊢ n ∈ {k | k ∉ AddSubmonoid.closure s} ∧ n ∈ upperBounds {k | k ∉ AddSubmonoid.closure s} ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s

Tactic:
upperBounds,

Goal state after:
n : ℕ
s : Set ℕ
⊢ n ∈ {k | k ∉ AddSubmonoid.closure s} ∧ n ∈ {x | ∀ ⦃a : ℕ⦄, a ∈ {k | k ∉ AddSubmonoid.closure s} → a ≤ x} ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s
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₁, S₁.multiplicity < S.multiplicity

Tactic:
obtain ⟨S', hS'⟩ := exists_Solution_of_Solution' (Solution'_descent S)
  exact ⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩

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

Goal state before:
pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]

Goal state after:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ (∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1)) * s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s) * s⁻¹
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h_cont.refine_2
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ x ^ (s + 1) ≠ 0

Tactic:
· exact (rpow_pos_of_pos ((Nat.cast_pos.mpr (by simp)).trans hx.1) _).ne'

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

Goal state before:
pp: case refine_1
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x ↦ (x - ↑(n + 1)) / x ^ (s + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

pp: case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x ↦ (x - ↑(n + 1)) / x ^ (1 + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

pp: case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ (x - ↑(n + 1)) / x ^ (s + 1) ≤ (x - ↑(n + 1)) / x ^ (1 + 1)

Tactic:
· exact (term_welldef n.succ_pos (zero_lt_one.trans_le hs)).1

Goal state after:
case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x ↦ (x - ↑(n + 1)) / x ^ (1 + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ (x - ↑(n + 1)) / x ^ (s + 1) ≤ (x - ↑(n + 1)) / x ^ (1 + 1)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
⊢ ↑(absNorm (∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (⨆ i, span {x i}))) *
      ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) =
    1

Tactic:
map_finprod _ <| hasFiniteMulSupport_fun_pow_multiplicity hx' (·),

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
⊢ ↑(∏ᶠ (i : FinitePlace K), absNorm (i.maximalIdeal.asIdeal ^ multiplicity i.maximalIdeal.asIdeal (⨆ i, span {x i}))) *
      ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) =
    1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ ↑(absNorm (v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (⨆ i, span {x i}))) * ⨆ i, v ↑(x i) = 1

Tactic:
multiplicity_iSup _ H,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ ↑(absNorm (v.maximalIdeal.asIdeal ^ ⨅ i, multiplicity v.maximalIdeal.asIdeal (span {x i}))) * ⨆ i, v ↑(x i) = 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
a : 𝓞 K
ha' : ↑m * a = ↑n * r
⊢ ↑m * (↑n * x) = ↑m * ↑a

Tactic:
rw [mul_left_comm, ← nsmul_eq_mul m, hmr]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
a : 𝓞 K
ha' : ↑m * a = ↑n * r
⊢ ↑n * ↑r = ↑m * ↑a
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 : ℕ
hn₁ : 0 < n
hn₂ : n < orderOf χ
⊢ gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)

Tactic:
by
  induction n, hn₁ using Nat.le_induction with
  | base => simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one]
  | succ n hn ih =>
      specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂
      have gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ =
            jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ := by
        have hχn : χ * (χ ^ n) ≠ 1 :=
          pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
        rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
      apply_fun (· * gaussSum χ ψ) at ih
      rw [mul_right_comm, ← pow_succ, gauss_rw] at ih
      rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 0 ∨ χ 0 = 0

Tactic:
by have := χ.map_zero'; tauto

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
⊢ hurwitzZetaOdd (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
have h3 : Gammaℂ (2 * k + 1) ≠ 0 := by
    refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)
    simp [pi_ne_zero]

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ hurwitzZetaOdd (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span {(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)}) =
    span ↑(Ideal.map (algebraMap R S) I) ⊔ span {(aeval x) Q}

Tactic:
span_eq,

Goal state after:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span {(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)}) =
    Ideal.map (algebraMap R S) I ⊔ span {(aeval x) Q}
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ 0 ≤ χ.zetaMul (p ^ k)

Tactic:
simp only [zetaMul, toArithmeticFunction, coe_zeta_mul_apply, coe_mk,
    Nat.sum_divisors_prime_pow hp, pow_eq_zero_iff', hp.ne_zero, ne_eq, false_and, ↓reduceIte,
    Nat.cast_pow, map_pow]
  rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h
  · refine Finset.sum_nonneg fun i _ ↦ ?_
    simp only [h, le_refl, pow_nonneg]
  · refine Finset.sum_nonneg fun i _ ↦ ?_
    simp only [h, one_pow, zero_le_one]
  · simp only [h, neg_one_geom_sum]
    split_ifs
    exacts [le_rfl, zero_le_one]

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

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

Tactic:
← LSeries_zeta_eq_riemannZeta hs,

Goal state after:
case e_a
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun n ↦ ↑(zeta n)) s = LSeries (⇑↑zeta) s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-s))

Tactic:
by
  have (p : Nat.Primes) : ‖χ p * (p : ℂ) ^ (-s)‖ ≤ (p : ℝ) ^ (-s).re := by
    simpa only [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
      using mul_le_of_le_one_left (by positivity) (χ.norm_le_one _)
  refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
    |>.of_norm.clog_one_sub.neg
  simp only [neg_re, neg_lt_neg_iff, hs]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ ((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I) = ↑(Real.sin (2 * π * ↑x✝ * x))

Tactic:
ofReal_sin,

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ ((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I) = sin ↑(2 * π * ↑x✝ * x)
Module: Mathlib.NumberTheory.LSeries.ZetaZeros

Goal state before:
pp: ⊢ riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ

Tactic:
have := riemannZetaZeros_codiscreteWithin_compl_one
  simp only [mem_codiscreteWithin, Set.mem_compl_iff, Set.mem_singleton_iff, sdiff_compl,
    Set.inf_eq_inter, Filter.disjoint_principal_right, mem_codiscrete, compl_compl] at this ⊢
  intro x
  rcases eq_or_ne x 1 with rfl | hx
  · exact riemannZeta_eventually_ne_zero_nhds_one.filter_mono nhdsWithin_le_nhds
  · exact Filter.mem_of_superset (this x hx)
      (by grind [riemannZeta_one_ne_zero, mem_riemannZetaZeros])

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
⊢ ↑(↑a * ↑x✝¹).val = (if (↑a * ↑x✝¹).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x✝¹).valMinAbs.natAbs

Tactic:
simp only [natCast_natAbs_valMinAbs]
        split_ifs <;> simp

Goal state after: