mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
obtain ⟨z, hz⟩ := S'.hcdvd
  rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.ha with
    ⟨x, hx⟩ | ⟨x, hx⟩ <;>
  rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.hb with
    ⟨y, hy⟩ | ⟨y, hy⟩
  · exfalso
    replace hζ : IsPrimitiveRoot ζ (3 ^ 1) := by rwa [pow_one]
    refine hζ.toInteger_sub_one_not_dvd_two (by decide) ⟨S'.u * λ ^ 2 * z ^ 3 - λ ^ 3 * (x + y), ?_⟩
    symm
    calc _ = S'.u * (λ * z) ^ 3 - λ ^ 4 * x - λ ^ 4 * y := by ring
    _ = (S'.a ^ 3 + S'.b ^ 3) - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) := by rw [← hx, ← hy, ← hz, ← S'.H]
    _ = 2 := by ring
  · left
    exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
  · right
    exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
  · exfalso
    replace hζ : IsPrimitiveRoot ζ (3 ^ 1) := by rwa [pow_one]
    refine hζ.toInteger_sub_one_not_dvd_two (by decide) ⟨λ ^ 3 * (x + y) - S'.u * λ ^ 2 * z ^ 3, ?_⟩
    symm
    calc _ = λ ^ 4 * x + λ ^ 4 * y - S'.u * (λ * z) ^ 3 := by ring
    _ = (S'.a ^ 3 + 1) + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy, ← hz, ← S'.H]
    _ = 2 := by ring

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - b ^ 2 = b ^ (p * 2) - b ^ 2

Tactic:
mul_comm

Goal state after:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (p * 2) - b ^ 2 = b ^ (p * 2) - b ^ 2
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p + b) * (b ^ p - b) = (b ^ p - b) * (b ^ p + b)

Tactic:
mul_comm

Goal state after:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ p - b) * (b ^ p + b)
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
⊢ p ≠ 0

Tactic:
by simp [hp.ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : (A * B - 1) * (b ^ 2 - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
mul_comm

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : (b ^ 2 - 1) * (A * B - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
n : ℕ
h : setGcd s ∣ n
m : ℕ
⊢ m ∈ insert n s → setGcd s ∣ m

Tactic:
by rintro (rfl | hm); exacts [h, setGcd_dvd_of_mem hm]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ ¬p ∣ b ^ 2 - 1

Tactic:
mul_comm

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ (b ^ 2 - 1) * b
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ ¬p ∣ b ^ 2 - 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
⊢ 2 * p ∣ A * B - 1

Tactic:
mul_comm

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : (b ^ 2 - 1) * (2 * p) ∣ (b ^ 2 - 1) * (A * B - 1)
⊢ 2 * p ∣ A * B - 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ λ * S.b = λ * S.b

Tactic:
mul_comm

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ S.b * λ = S.b * λ
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝¹ : P.IsMaximal
this✝ : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬P ∣ differentIdeal A B
this : Algebra.IsSeparable (A ⧸ Ideal.under A P) (B ⧸ P)
⊢ Algebra.IsSeparable (Ideal.under A P).ResidueField P.ResidueField

Tactic:
infer_instance

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

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

Tactic:
have h := Nat.exists_infinite_primes (b * (b ^ 2 - 1) + 1 + m)

Goal state after:
case pos
b : ℕ
h✝ : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
h : ∃ p, b * (b ^ 2 - 1) + 1 + m ≤ p ∧ Prime p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n
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
h : λ ∣ S.w
⊢ λ * λ ^ S.multiplicity ∣ S.c

Tactic:
mul_comm

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ S.w
⊢ λ ^ S.multiplicity * λ ∣ S.c
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
h₁ : IsCoprime (S.x * S.y) S.z
⊢ S.w ^ 3 * ↑S.u = ↑S.u * S.w ^ 3

Tactic:
mul_comm

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h₁ : IsCoprime (S.x * S.y) S.z
⊢ ↑S.u * S.w ^ 3 = ↑S.u * S.w ^ 3
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
⊢ mulHeight 1 = 1

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
hι : IsEmpty ι
⊢ mulHeight 1 = 1

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
hι : Nonempty ι
⊢ mulHeight 1 = 1
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 : ι'
⊢ ∑ i, (⨆ ji, v (A ji)) * ⨆ i, v (x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

pp: 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)

Tactic:
case h =>
    gcongr
    · exact Real.iSup_nonneg_of_nonnegHomClass v _
    · exact Finite.le_ciSup_of_le (j, i) le_rfl
    · exact Finite.le_ciSup_of_le i le_rfl

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)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
⊢ ⨆ i, v (A (j, ↑i)) * v (x ↑i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
rw [this fun i ↦ v (A (j, i)) * v (x i)]

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
⊢ ⨆ i, v (A (j, i)) * v (x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Goal state after:
case inl
K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

case inr
K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (∏ a, (Multiset.map (fun i ↦ ⨆ i_1, i (x a i_1)) archAbsVal).prod) * ∏ b, ∏ᶠ (a : ↑nonarchAbsVal), ⨆ i, ↑a (x b i) =
    ∏ a, mulHeight (x a)

Tactic:
← prod_mul_distrib

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ ∏ x_1, (Multiset.map (fun i ↦ ⨆ i_1, i (x x_1 i_1)) archAbsVal).prod * ∏ᶠ (a : ↑nonarchAbsVal), ⨆ i, ↑a (x x_1 i) =
    ∏ a, mulHeight (x a)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : IsEmpty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
Module: Mathlib.NumberTheory.Height.Projectivization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
a b : { v // v ≠ 0 }
t : K
h : ↑a = t • ↑b
⊢ t ≠ 0

Tactic:
by
    contrapose! h
    simpa [h] using a.prop

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

Goal state before:
pp: this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / 0
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
div_zero,

Goal state after:
this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 0
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 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
⊢ ∑ x ∈ univ \ {1}, χ (x / (1 - x)) + χ (1 / 0) = -χ (-1)

Tactic:
div_zero,

Goal state after:
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
⊢ ∑ x ∈ univ \ {1}, χ (x / (1 - x)) + χ 0 = -χ (-1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ↑(Fintype.card F) ≠ 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : ψ.IsPrimitive
⊢ jacobiSum χ φ * gaussSum (χ * φ) ψ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
mul_comm

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ↑(Fintype.card F) ≠ 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : ψ.IsPrimitive
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
convert EventuallyEq.deriv_eq (f := fun s ↦ (s - 1)⁻¹ + riemannZeta₀ s) ?_

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)⁻¹ + riemannZeta₀ s) s

case convert_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ riemannZeta =ᶠ[𝓝 s] fun s ↦ (s - 1)⁻¹ + riemannZeta₀ s
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ ∀ᶠ (s : ℂ) in 𝓝[≠] 1, deriv riemannZeta s / riemannZeta s = -(s - 1)⁻¹ + deriv riemannZeta₁ s / riemannZeta₁ s

Tactic:
filter_upwards [eventually_mem_nhdsWithin,
    riemannZeta₁_ne_zero_of_near_one.filter_mono nhdsWithin_le_nhds]
  grind [deriv_riemannZeta_eq_neg_inv_sub_sq_mul_add, riemannZeta_eq_inv_sub_mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : (∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i) ≤ B
⊢ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ ↑n ^ totalWeight K * B

Tactic:
mul_comm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : (∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)) * ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ B
⊢ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ ↑n ^ totalWeight K * B
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 : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
⊢ eval₂ i x X = x

Tactic:
eval₂_X

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
⊢ x = x
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 : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ (h.basis.repr (h.basis ⟨n, hn⟩)) ⟨i, hi⟩ = Pi.single (↑⟨n, hn⟩) 1 ↑⟨i, ?m.131⟩

Tactic:
rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]

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

Goal state before:
pp: case inr
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : s ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
exact LFunction_changeLevel_aux hMN χ h

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunction ((changeLevel ⋯) 1) s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * LFunction 1 s

Tactic:
mul_comm

Goal state after:
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunction ((changeLevel ⋯) 1) s = LFunction 1 s * ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    ↑N ^ (s - 1 / 2) * ((gaussSum χ stdAddChar / I ^ if χ.Even then 0 else 1) / ↑N ^ (1 / 2)) * completedLFunction χ⁻¹ s

Tactic:
← mul_comm_div,

Goal state after:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    ↑N ^ (s - 1 / 2) / ↑N ^ (1 / 2) * (gaussSum χ stdAddChar / I ^ if χ.Even then 0 else 1) * completedLFunction χ⁻¹ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    ↑N ^ (s - 1 / 2) / ↑N ^ (1 / 2) * (gaussSum χ stdAddChar / I ^ if χ.Even then 0 else 1) * completedLFunction χ⁻¹ s

Tactic:
← mul_comm_div,

Goal state after:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    (↑N ^ (s - 1 / 2) / ↑N ^ (1 / 2) / I ^ if χ.Even then 0 else 1) * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case pos
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)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
⊢ Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count J
      (Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)

Tactic:
refine this.trans ?_
    -- Get rid of the `map` by applying the equiv to both sides.
    generalize hJ' :
      (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
    have : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J' : Ideal S) =
        J := by
      rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk]
    subst this
    -- Get rid of the `attach` by applying the subtype `coe` to both sides.
    rw [Multiset.count_map_eq_count' fun f =>
        ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f :
          Ideal S),
      Multiset.count_attach]
    · exact Subtype.coe_injective.comp (Equiv.injective _)

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case pos.ha
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)
this :
  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))
⊢ Irreducible J

pp: case pos.hb
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)
this :
  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))
⊢ Ideal.map (algebraMap R S) I ≠ 0

Tactic:
· exact irreducible_of_normalized_factor _ hJ

Goal state after:
case pos.hb
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)
this :
  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))
⊢ Ideal.map (algebraMap R S) I ≠ 0
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f + g) s = LSeries f s + LSeries g s

Tactic:
by
  simpa [LSeries, term_add] using hf.tsum_add hg

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (-f) s

Tactic:
simpa [LSeriesSummable, term_neg] using! Summable.neg hf

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

Goal state before:
pp: case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x * (↑↑m ^ ↑x)⁻¹ = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

Tactic:
mul_comm

Goal state after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹