mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case refine_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ IsCoprime ↑a ↑b

pp: case refine_5
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ ↑a ^ 3 + ↑b ^ 3 = ↑1 * ↑c ^ 3

Tactic:
· exact IsCoprime.intCast hcoprime

Goal state after:
case refine_5
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ ↑a ^ 3 + ↑b ^ 3 = ↑1 * ↑c ^ 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ (quadraticChar (ZMod p)) 2 = χ₈ ↑p

Tactic:
quadraticChar_two ((ringChar_zmod_n p).substr hp),

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ χ₈ ↑(Fintype.card (ZMod p)) = χ₈ ↑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 K L) ((algebraMap A K) y)) ∈ ↑p

Tactic:
← IsScalarTower.algebraMap_apply,

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) (x * (algebraMap A L) y) ∈ ↑p
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
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 : IsCoprime 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 ≠ ⊥
x : B
hx : x ∈ a
this✝² : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : IsScalarTower A (A ⧸ p) (B ⧸ a)
this✝ : Module.Finite (A ⧸ p) (B ⧸ a)
this : Prime P
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ a :=
  let __spread.0 := (Ideal.quotEquivOfEq ha).trans (P.quotientMulEquivQuotientProd a hPa);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
hx' : (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).2 = 0
⊢ (Algebra.trace (A ⧸ p) (B ⧸ P)) (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).1 +
      (Algebra.trace (A ⧸ p) (B ⧸ a)) (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).2 =
    0

Tactic:
Algebra.trace_eq_zero_of_not_isSeparable H,

Goal state after:
case neg
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 : IsCoprime 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 ≠ ⊥
x : B
hx : x ∈ a
this✝² : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : IsScalarTower A (A ⧸ p) (B ⧸ a)
this✝ : Module.Finite (A ⧸ p) (B ⧸ a)
this : Prime P
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ a :=
  let __spread.0 := (Ideal.quotEquivOfEq ha).trans (P.quotientMulEquivQuotientProd a hPa);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
hx' : (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).2 = 0
⊢ 0 (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).1 +
      (Algebra.trace (A ⧸ p) (B ⧸ a)) (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).2 =
    0
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : ¬0 ≤ a i
⊢ r ≤ setGcd s * (x / setGcd s)

Tactic:
Nat.mul_div_cancel' (setGcd_dvd_of_mem hxs)

Goal state after:
case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : ¬0 ≤ a i
⊢ r ≤ x
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
by_cases b_ge_two : 2 ≤ b

Goal state after:
case pos
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: y : ℝ
hy : 1 ≤ y
⊢ ↑(harmonic ⌊y⌋₊) ≤ 1 + Real.log y

Tactic:
refine (harmonic_le_one_add_log _).trans ?_
  gcongr
  · exact_mod_cast Nat.floor_pos.mpr hy
  · exact Nat.floor_le <| zero_le_one.trans hy

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ x_1, v (A (j, x_1)) * v (x x_1) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
Finset.sum_le_sum (g := fun _ ↦ (⨆ ji, v (A ji)) * ⨆ i, v (x i)) fun i _ ↦ ?h

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ i, (⨆ ji, v (A ji)) * ⨆ i, v (x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

case h
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
i : ι
x✝ : i ∈ Finset.univ
⊢ v (A (j, i)) * v (x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case zero
⊢ termSum 1 0 = log (↑0 + 1) - ↑(harmonic (0 + 1)) + 1

Tactic:
simp_rw [termSum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]

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ζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.u₄ ^ 2 = 1

Tactic:
rcases S.u₄_eq_one_or_neg_one with h | h <;> simp [h]

Goal state after:
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
⊢ ∀ᶠ (x : ℂ) in 𝓝 1, x ∈ {1}ᶜ → ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)

Tactic:
filter_upwards [this] with a 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✝ : a ∈ {1}ᶜ
⊢ ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case ha
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
j : ι'
⊢ 0 ≤ (⨆ i, ↑v (x i)) ^ N

pp: case hbc
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
j : ι'
⊢ ⨆ s, ↑v (coeff (↑s) (p j)) ≤ ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
· exact HH₁ v.val

Goal state after:
case hbc
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
j : ι'
⊢ ⨆ s, ↑v (coeff (↑s) (p j)) ≤ ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 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
hx : x ≠ 0
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
by
  obtain ⟨i₀, hi₀⟩ := Function.ne_iff.mp hx
  let i' : { j // (x j : K) ≠ 0 } := ⟨i₀, mod_cast hi₀⟩
  have : Nonempty _ := .intro i'
  have hI : span (Set.range x) = span (Set.range fun i : { j // (x j : K) ≠ 0 } ↦ x i.val) := by
    convert span_range_eq_span_range_support x <;> norm_cast
  have hx₀ : (fun i ↦ (x i : K)) ≠ 0 := Function.ne_iff.mpr ⟨_, i'.prop⟩
  simp_rw [Finite.iSup_eq_iSup_subtype hx₀, hI]
  exact absNorm_mul_finprod_finitePlace_eq_one_aux fun j ↦ mod_cast j.prop

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

Goal state before:
pp: case e'_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ -(s - 1)⁻¹ ^ 2 + deriv riemannZeta₀ s = deriv (fun s ↦ (s - 1)⁻¹ + riemannZeta₀ s) s

Tactic:
deriv_fun_add (by fun_prop) (by fun_prop),

Goal state after:
case e'_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ -(s - 1)⁻¹ ^ 2 + deriv riemannZeta₀ s = deriv (fun s ↦ (s - 1)⁻¹) s + deriv riemannZeta₀ s
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:

Tactic:
_ ≤ n ^ (totalWeight K - 1) * ⨆ i, v (![(x : K), n] i) := by
      gcongr; exact Finite.le_ciSup_of_le 0 le_rfl
    _ ≤ (∏ v' ∈ univ.erase v, (⨆ i, v' (![↑x, ↑n] i)) ^ v'.mult) *
         (⨆ i, v (![↑x, ↑n] i)) ^ (v.mult - 1) * ⨆ i, v (![(x : K), n] i) := by
      rw [pow_totalWeight_sub_one_eq hn]
      gcongr
      · exact Real.iSup_nonneg_of_nonnegHomClass ..
      · exact prod_nonneg fun _ _ ↦ pow_nonneg (Real.iSup_nonneg_of_nonnegHomClass ..) _
      all_goals exact Finite.le_ciSup_of_le 1 <| by simp
    _ ≤ B := by
      rwa [mul_assoc, pow_sub_one_mul v.mult_ne_zero, prod_erase_mul _ _ (mem_univ v)]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h h' : IsAdjoinRoot S f
eq : ∀ (x : R[X]), h.map x = h'.map x
⊢ h = h'

Tactic:
cases h; cases h'; congr
  exact AlgHom.ext eq

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

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ¬ψ = 1
⊢ jacobiSum 1 ψ = -1 + 0 * (μ - 1) ^ 2

Tactic:
jacobiSum_one_nontrivial hψ₀,

Goal state after:
case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ¬ψ = 1
⊢ -1 = -1 + 0 * (μ - 1) ^ 2
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ emultiplicity J (Ideal.map (algebraMap R S) I) =
    emultiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))

Tactic:
classical
  rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, Equiv.coe_trans, Function.comp_apply,
    Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity,
    IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
m : bernoulliFun k (2 * 2⁻¹) = 2 ^ k / 2 * ∑ x ∈ Finset.range 2, bernoulliFun k (2⁻¹ + ↑x / 2)
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
mul_inv_cancel₀ (two_ne_zero' ℝ),

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : bernoulliFun k 1 = 2 ^ k / 2 * ∑ x ∈ Finset.range 2, bernoulliFun k (2⁻¹ + ↑x / 2)
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_a.e_f.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
hi : i ≠ 0
⊢ Φ i * hurwitzZetaEven (toAddCircle i) s = Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)

Tactic:
rw [hurwitzZetaEven_def_of_ne_or_ne (.inl (hi ∘ toAddCircle_eq_zero.mp))]

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s = term f s + term g s

Tactic:
by
  ext ⟨- | n⟩ <;>
  simp [add_div]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * ∑' (a : Nat.Primes), (-log (1 - 1 ↑↑a * ↑↑a ^ (-(1 + ↑x)))).re +
        4 * ∑' (a : Nat.Primes), (-log (1 - χ ↑↑a * ↑↑a ^ (-(1 + ↑x + I * ↑y)))).re +
      (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))).re

Tactic:
re_tsum H₂,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * ∑' (a : Nat.Primes), (-log (1 - 1 ↑↑a * ↑↑a ^ (-(1 + ↑x)))).re +
        4 * ∑' (a : Nat.Primes), (-log (1 - χ ↑↑a * ↑↑a ^ (-(1 + ↑x + I * ↑y)))).re +
      ∑' (a : Nat.Primes), (-log (1 - (χ ^ 2) ↑↑a * ↑↑a ^ (-(1 + ↑x + 2 * I * ↑y)))).re
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case hbc
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 2 ≤ ↑↑p

Tactic:
exact Nat.ofNat_le_cast.mpr p.prop.two_le

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k

Tactic:
← insert_Icc_add_one_left_eq_Icc n.zero_le,

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ ∑ k ∈ insert 0 (Icc (0 + 1) n), f k = ∑ k ∈ Icc 1 n, f k
Module: Mathlib.NumberTheory.LSeries.ZetaZeros

Goal state before:
pp: ⊢ riemannZetaZerosᶜ ∈ Filter.codiscreteWithin {1}ᶜ

Tactic:
refine analyticOn_riemannZeta.preimage_zero_mem_codiscreteWithin (x := 2) ?_ (by simp) ?_

Goal state after:
case refine_1
⊢ riemannZeta 2 ≠ 0

case refine_2
⊢ IsConnected {1}ᶜ
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs

Tactic:
simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
⊢ x ∈ I ↔ x ∈ (f ∘ₗ g).ker

Tactic:
simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
      f, g]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
⊢ x ∈ I ↔ x * ϖ ^ n ∈ I * I ^ n
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
| legendreSym p (a % ↑b)

Tactic:
rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <|
            dvd_of_mem_primeFactorsList hp), ← legendreSym.mod]

Goal state after:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
| legendreSym p a
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑a | b) = J(↑a | b % (4 * a))

Tactic:
ha₂

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑a | b) = J(↑(2 ^ e * a') | b % (4 * a))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑a | b) = J(↑(2 ^ e * a') | b % (4 * a))

Tactic:
ha₂

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑(2 ^ e * a') | b) = J(↑(2 ^ e * a') | b % (4 * a))