mathlib-initiative/mathlib-tactics huggingface dataset:
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 ≠ ⊥
this✝¹ : Ideal.map (algebraMap A B) p ∣ a ^ e
this✝ : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
this : (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
⊢ (Algebra.trace K L) (x * (algebraMap B L) ((algebraMap A B) y)) ∈ ↑p

Tactic:
← hz'

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
this✝ : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
this : (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
⊢ (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 ≤ |v w w| - v w w

Tactic:
rw [sub_nonneg]
      exact le_abs_self _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  (QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₁✝)) =
    (QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₂✝))
⊢ a₁✝ = a₂✝

Tactic:
exact (EmbeddingLike.apply_eq_iff_eq _).mp <| (QuotientGroup.kerLift_injective _).eq_iff.mp h

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)) = ↑((logEmbeddingEquiv K) ((basisModTorsion K) i))

Tactic:
← fundSystem_mk,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ (logEmbedding K) (Additive.ofMul (fundSystem K i)) = ↑((logEmbeddingEquiv K) (Additive.ofMul ↑(fundSystem K i)))
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
⊢ Additive.ofMul ↑(ζ * ∏ i, fundSystem K i ^ f i) = ∑ i, f i • Additive.ofMul ↑(fundSystem K i)

Tactic:
QuotientGroup.mk_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
⊢ Additive.ofMul (↑ζ * ↑(∏ i, fundSystem K i ^ f i)) = ∑ i, f i • Additive.ofMul ↑(fundSystem K i)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ ↑ζ = 1

Tactic:
QuotientGroup.mk_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ ↑x * ↑(∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹ = 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
h_tors : ζ ∈ torsion K
⊢ ∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (fun ζe ↦ x = ↑ζe.1 * ∏ i, fundSystem K i ^ ζe.2 i) y →
      y = (⟨ζ, h_tors⟩, ⇑((basisModTorsion K).repr (Additive.ofMul ↑x)))

Tactic:
rintro ⟨⟨ζ', h_tors'⟩, η⟩ hf
    simp only [ζ, ← fun_eq_repr K h_tors' hf, Prod.mk.injEq, Subtype.mk.injEq, and_true]
    nth_rewrite 1 [hf]
    rw [_root_.mul_inv_cancel_right]

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

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : {a, b, c}.gcd id = 1
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ 3 ∣ b

Tactic:
refine three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2 ha ?_ h3a HF H

Goal state after:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : {a, b, c}.gcd id = 1
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ {a, b, c}.gcd id = 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) a = 0

Tactic:
ha

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) 0 = 0
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
⊢ P * P ∣ Ideal.map (algebraMap A B) p

Tactic:
ha

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
⊢ P * P ∣ P * a
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: P : Ideal ℕ
⊢ P.IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ p, Nat.Prime p ∧ P = span {p}

Tactic:
refine .symm ⟨?_, fun h ↦ or_iff_not_imp_left.mpr fun h0 ↦ or_iff_not_imp_right.mpr fun hsp ↦
    (le_maximalIdeal h.ne_top).antisymm fun n hn ↦ ?_⟩

Goal state after:
case refine_1
P : Ideal ℕ
⊢ (P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ p, Nat.Prime p ∧ P = span {p}) → P.IsPrime

case refine_2
P : Ideal ℕ
h : P.IsPrime
h0 : ¬P = ⊥
hsp : ¬∃ p, Nat.Prime p ∧ P = span {p}
n : ℕ
hn : n ∈ maximalIdeal ℕ
⊢ n ∈ P
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)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
this : (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
⊢ (Algebra.trace K L) (x * (algebraMap B L) ((algebraMap A B) y)) ∈ ↑p

Tactic:
← hz'

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)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
this : (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
⊢ (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
⊢ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal → a ≠ 0

Tactic:
ha

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
ha : a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal
⊢ a ≠ 0
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
ha : a = 0
⊢ a ∉ Multiset.map (fun v ↦ max (v x) 1) archAbsVal

Tactic:
ha

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
ha : a = 0
⊢ 0 ∉ Multiset.map (fun v ↦ max (v x) 1) archAbsVal
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.refine_1
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
⊢ 1 ≤ ⨆ i_1, v (((x i)⁻¹ • x) i_1)

Tactic:
refine Finite.le_ciSup_of_le i <| le_of_eq ?_

Goal state after:
case inr.refine_1
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
⊢ 1 = v (((x i)⁻¹ • x) i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: f : Fin 2 → ℝ
⊢ iSup ![f 0, f 1] = max (![f 0, f 1] 0) (![f 0, f 1] 1)

Tactic:
exact (max_eq_iSup ..).symm

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

Goal state before:
pp: K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
u : (NumberField.RingOfIntegers K)ˣ
hc : c ≠ 0
⊢ ¬hζ.toInteger - 1 ∣ a → ¬hζ.toInteger - 1 ∣ b → hζ.toInteger - 1 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ ↑u * c ^ 3

Tactic:
ha

Goal state after:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
u : (NumberField.RingOfIntegers K)ˣ
hc : c ≠ 0
ha : ¬hζ.toInteger - 1 ∣ a
⊢ ¬hζ.toInteger - 1 ∣ b → hζ.toInteger - 1 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ ↑u * c ^ 3
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ termTSum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
by
  apply HasSum.tsum_eq
  rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) s)]
  change Tendsto (fun N ↦ termSum s N) atTop _
  simp_rw [termSum_of_lt _ hs]
  apply Tendsto.sub
  · rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]
    simp_rw [mul_sub, mul_one]
    refine tendsto_const_nhds.sub (Tendsto.const_mul _ ?_)
    refine tendsto_const_nhds.div_atTop <| (tendsto_rpow_atTop (by linarith)).comp ?_
    exact tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop
  · rw [← sub_zero (tsum _)]
    apply (((Summable.hasSum ?_).tendsto_sum_nat).sub ?_).const_mul
    · exact_mod_cast (summable_nat_add_iff 1).mpr (summable_one_div_nat_rpow.mpr hs)
    · apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
              (h := fun n : ℕ ↦ (1 / ↑(n + 1) : ℝ) ^ (s - 1))
      · rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]
        refine Tendsto.rpow_const ?_ (Or.inr <| by linarith)
        exact (tendsto_const_div_atTop_nhds_zero_nat _).comp (tendsto_add_atTop_nat _)
      · intro n
        positivity
      · intro n
        dsimp only
        transitivity (n + 1) / (n + 1) ^ s
        · gcongr
          linarith
        · apply le_of_eq
          rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]
          · norm_cast
          all_goals positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ logHeight₁ (-x) = logHeight₁ x

Tactic:
by
  simp [logHeight₁_eq_log_mulHeight₁, mulHeight₁_neg]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
n' : ℕ
hn : k < n' + 1
hμ : IsPrimitiveRoot μ (n' + 1)
⊢ ∃ z ∈ ℤ[μ], ↑(n' + 1) = z * (μ - 1) ^ k

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.le_of_lt_succ hn)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
⊢ ∃ z ∈ ℤ[μ], ↑(m + k + 1) = z * (μ - 1) ^ k
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
⊢ a ∈ Ioi 1 → ↑a ∈ {1}ᶜ

Tactic:
ha

Goal state after:
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ↑a ∈ {1}ᶜ
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this✝ : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : {z | 0 < z.re} ∈ 𝓝 1
a : ℂ
⊢ 0 < a.re → a ∈ {1}ᶜ → ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)

Tactic:
ha

Goal state after:
h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this✝ : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : {z | 0 < z.re} ∈ 𝓝 1
a : ℂ
ha : 0 < a.re
⊢ a ∈ {1}ᶜ → ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
rw [gaussSum_mul _ _ ψ, sum_eq_sum_sdiff_singleton_add (mem_univ (0 : F))]
  conv =>
    enter [2, 2, 2, x]
    rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]
  rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
  have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t =
      (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t := by
    intro t ht
    simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
    exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm
  simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
  conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
  simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
  rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_sdiff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, zero_mul, add_zero]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (InfinitePlace K)
n : ℕ
hn : n ≠ 0
v : InfinitePlace K
⊢ ↑n ^ (totalWeight K - 1) = (∏ w ∈ univ.erase v, ↑n ^ w.mult) * ↑n ^ (v.mult - 1)

Tactic:
by
  refine mul_right_cancel₀ (b := (n : ℝ)) (mod_cast hn) ?_
  rw [pow_sub_one_mul (totalWeight_pos K).ne', totalWeight_eq_sum_mult, ← prod_pow_eq_pow_sum,
    ← prod_erase_mul _ _ (mem_univ v), ← pow_sub_one_mul v.mult_ne_zero, ← mul_assoc]

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

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / (2 * (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * ↑k + 1) / ((2 * ↑k + 1) * 2 * Complex.Gamma (2 * ↑k + 1))

Tactic:
rw [(by simp : 2 * (k : ℂ) + 1 = ↑(2 * k + 1)), cpow_natCast]

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / (2 * ↑(2 * k + 1) * Complex.Gamma ↑(2 * k + 1)) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / (↑(2 * k + 1) * 2 * Complex.Gamma ↑(2 * k + 1))
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ (if Nat.Prime (↑pk.1 ^ (pk.2 + 1 + 1)) then 0 else Λ (↑pk.1 ^ (pk.2 + 1 + 1))) / ↑↑pk.1 ^ (pk.2 + 1 + 1)

Tactic:
positivity [vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))]

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

Goal state before:
pp: case inl
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
k : ℕ
H : n + 1 < k
⊢ Tendsto (fun x ↦ F x k) atTop (nhds 0)

Tactic:
have H₀ : (0 : ℝ) ≤ k / (n + 1) := by positivity
      have H₀' : (0 : ℝ) ≤ (n + 1) / k := by positivity
      have H₁ : (k / (n + 1) : ℂ) = (k / (n + 1) : ℝ) := by push_cast; rfl
      have H₂ : (n + 1) / k < (1 : ℝ) :=
        (div_lt_one <| mod_cast n.succ_pos.trans H).mpr <| mod_cast H
      simp only [Set.mem_ofPred_eq, H, Set.indicator_of_mem, F]
      conv =>
        enter [1, x]
        rw [div_eq_mul_inv, H₁, ← ofReal_cpow H₀, ← ofReal_inv, ← Real.inv_rpow H₀, inv_div]
      conv => enter [3, 1]; rw [← mul_zero (f k)]
      exact
        (tendsto_rpow_atTop_of_base_lt_one _ (neg_one_lt_zero.trans_le H₀') H₂).ofReal.const_mul _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ (fun n ↦ 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4))) = fun n ↦ 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)

Tactic:
ext1 n
    ring_nf

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

Goal state before:
pp: q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ a [MOD q]

Tactic:
frequently_atTop

Goal state after:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ Prime b ∧ b ≡ a [MOD q]
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ a [MOD q]

Tactic:
by
  rw [frequently_atTop]
  intro n
  obtain ⟨p, hn, hp, ha⟩ := forall_exists_prime_gt_and_modEq n hq h
  exact ⟨p, hn.le, hp, ha⟩

Goal state after: