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

Goal state before:
pp: case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ False

Tactic:
refine H (-b) (-c) a ha (by simp [h3b]) (by simp [h3c]) h3a hbc ?_

Goal state after:
case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ (-b) ^ 3 + (-c) ^ 3 = a ^ 3
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:
let : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap (by
      rw [← Ideal.map_le_iff_le_comap, ← hP]
      exact Ideal.mul_le_right)

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
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)
this : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ (3 ^ 2 ^ (2 ^ n - 1)) ^ 2 = 1

Tactic:
← key,

Goal state after:
case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ (3 ^ 2 ^ (2 ^ n - 1)) ^ 2 = 1
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ 2 ^ (2 ^ n - 1) ≠ 1

Tactic:
← key,

Goal state after:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ 2 ^ (2 ^ n - 1) ≠ 1
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ p, Nat.Prime p ∧ P = span {p}
n : ℕ
hn : n ∈ maximalIdeal ℕ
p : ℕ := Nat.find h0
⊢ n ∈ P

Tactic:
have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0

Goal state after:
case refine_2
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ p, Nat.Prime p ∧ P = span {p}
n : ℕ
hn : n ∈ maximalIdeal ℕ
p : ℕ := Nat.find h0
hp : p ∈ P
hp0 : p ≠ 0
⊢ n ∈ P
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:
rw [mul_comm] at ha₅

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.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
⊢ mulHeight x = mulHeight fun i ↦ x ↑i

Tactic:
by
  classical
  let e := Equiv.Set.sumCompl x.support
  have hx : x ∘ e = Sum.elim (fun i : x.support ↦ x i.val) 0 := by
    ext1 i
    simp only [comp_apply]
    cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop
  rw [← mulHeight_comp_equiv e, hx]
  exact mulHeight_sumElim_zero_eq ..

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

Goal state before:
pp: case inr.inr
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)
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
have HH₁ (v : AbsoluteValue K ℝ) : 0 ≤ (⨆ i, v (x i)) ^ N :=
    pow_nonneg (Real.iSup_nonneg_of_nonnegHomClass v _) N

Goal state after:
case inr.inr
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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N
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
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
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
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
j : ι'
⊢ ((p j).coeff.sum fun x c ↦ v c) ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c

Tactic:
· exact HH₁ v

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
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
j : ι'
⊢ ((p j).coeff.sum fun x c ↦ v c) ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : w ∈ (multisetInfinitePlace K).toFinset
⊢ f w ^ Multiset.count w (multisetInfinitePlace K) = f ↑⟨w, ⋯⟩ ^ InfinitePlace.mult ⟨w, ⋯⟩

Tactic:
count_multisetInfinitePlace_eq_mult ⟨w, _⟩

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : w ∈ (multisetInfinitePlace K).toFinset
⊢ f w ^ InfinitePlace.mult ⟨w, ?m.91⟩ = f ↑⟨w, ⋯⟩ ^ InfinitePlace.mult ⟨w, ⋯⟩

K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : w ∈ (multisetInfinitePlace K).toFinset
⊢ ∃ φ, place φ = w
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case inl
⊢ riemannZeta ((starRingEnd ℂ) 1) = (starRingEnd ℂ) (riemannZeta 1)

Tactic:
have h : riemannZeta 1 = ((γ - Real.log (4 * π)) / 2 : ℝ) := by
      rw [riemannZeta_one, ofReal_div, ofReal_sub, ofReal_log (by positivity : (0 : ℝ) ≤ 4 * π)]
      norm_cast
    rw [map_one, h, conj_ofReal]

Goal state after:
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, χ (x / (1 - x)) = -χ (-1)

Tactic:
rw [sum_eq_sum_sdiff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_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)) = -χ (-1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case refine_2
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
y : F
hy : ¬y = -1
⊢ ¬y / (1 + y) = 1

Tactic:
div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h,

Goal state after:
case refine_2
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
y : F
hy : ¬y = -1
⊢ ¬y = 1 * (1 + y)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b]

Tactic:
show c = 0 from congrFun hcd 0,

Goal state after:
case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ mulHeight ![a * 0, a * d + b * 0, b * d] ≤ max C 1 * mulHeight ![a, b]
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ ∀ a ∈ {1}ᶜ, riemannZeta a = (a - 1)⁻¹ + riemannZeta₀ a

Tactic:
by grind [riemannZeta_eq_inv_sub_add]

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
⊢ x ∈ (fun a ↦ ↑a / ↑n) '' {a | mulHeight ![↑a, ↑n] ≤ B}

Tactic:
simp only [Set.mem_ofPred_eq, Set.mem_image]
    obtain ⟨a, ha⟩ : ∃ a : 𝓞 K, n * x = a := ⟨⟨_, hx₁⟩, rfl⟩
    refine ⟨a, ?_, (EuclideanDomain.eq_div_of_mul_eq_right hn' ha).symm⟩
    rwa [← ha, ← mulHeight₁_div_eq_mulHeight, mul_div_cancel_left₀ x hn']

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 : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx✝ hx : eval₂ i x f = 0
⊢ eval₂ i x (h.repr 1) = 1

Tactic:
simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_one _)]

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

Goal state before:
pp: q : ℚ
⊢ mulHeight ![q, 1] = mulHeight ![↑q.num, ↑q.den]

Tactic:
by
  have hq₀ : (q.den : ℚ) ≠ 0 := mod_cast q.den_nz
  rw [← mulHeight_smul_eq_mulHeight _ hq₀]
  simp

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑j.val + ↑N * ↑m) ^ s = Φ ↑(j.val + N * m) / ↑(j.val + N * m) ^ s

Tactic:
by
    simp only [Nat.cast_add, Nat.cast_mul, natCast_zmod_val, natCast_self, zero_mul, add_zero]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ContinuousWithinAt (LFunctionTrivChar₁ n) {1}ᶜ 1

Tactic:
simpa using LFunctionTrivChar_residue_one

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

Goal state before:
pp: case pos
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : -j ≠ 0 ∨ s ≠ 1
⊢ Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

pp: case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : ¬(-j ≠ 0 ∨ s ≠ 1)
⊢ Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Tactic:
· rw [LFunction_stdAddChar_eq_expZeta _ _ h]

Goal state after:
case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : ¬(-j ≠ 0 ∨ s ≠ 1)
⊢ Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case zero
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
x : ℝ
⊢ 1 = (↑m)⁻¹ * ↑m

Tactic:
rw [inv_mul_cancel₀ (Nat.cast_ne_zero.mpr m0)]

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k)! = ↑((2 * k - 1 + 1) * (2 * k - 1)!)

Tactic:
← Nat.factorial_succ,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k)! = ↑(2 * k - 1 + 1)!
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
t : ℂ
ht : t ∈ {1}ᶜ
⊢ DifferentiableAt ℂ B.F t

Tactic:
exact B.F_differentiableAt_of_ne ht

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

Goal state before:
pp: case e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * (↑n ^ ↑(-x) * ↑n ^ (↑2 * -(I * ↑y))) = ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2

Tactic:
cpow_nat_mul,

Goal state after:
case e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * (↑n ^ ↑(-x) * (↑n ^ (-(I * ↑y))) ^ 2) = ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
⊢ 0 ≤
    3 * (-log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re

Tactic:
by
  by_cases hn' : IsUnit (n : ZMod N)
  · have hn : (n : ℝ) ^ (-x) < 1 := by
      rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]
      exact .inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx
    have hz : ‖χ n * (n : ℂ) ^ (-(I * y))‖ = 1 := by
      rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit,
        ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (mod_cast by lia)]
      simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
        neg_zero, Real.rpow_zero, one_mul]
    rw [MulChar.one_apply hn', one_mul]
    convert! re_log_comb_nonneg' (by positivity) hn hz using 6
    · simp only [ofReal_cpow n.cast_nonneg (-x), ofReal_natCast, ofReal_neg]
    · congr 2
      rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, mul_left_comm]
    · rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
  · simp only [MulChar.map_nonunit _ hn', zero_mul, sub_zero, log_one, neg_zero, zero_re, mul_zero,
      neg_add_rev, add_zero, pow_two, le_refl]

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

Goal state before:
pp: a₁ a₂ : ℤ
b : ℕ
⊢ J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b)

Tactic:
simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul]

Goal state after:
a₁ a₂ : ℤ
b : ℕ
⊢ (List.map (fun x ↦ legendreSym (↑x) a₁ * legendreSym (↑x) a₂) b.primeFactorsList.attach).prod =
    (List.map (fun x ↦ legendreSym (↑x) a₁) b.primeFactorsList.attach).prod *
      (List.map (fun x ↦ legendreSym (↑x) a₂) b.primeFactorsList.attach).prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ Int.gcd 0 ↑b ≠ 1

Tactic:
rw [Int.gcd_zero_left, Int.natAbs_natCast]

Goal state after:
b : ℕ
hb : 1 < b
⊢ b ≠ 1
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x 1 ∪ (Set.Icc y⁻¹ 1)⁻¹

Tactic:
rw [Set.inv_Icc, inv_one, Set.Icc_union_Icc_eq_Icc] <;>
      simp [h, hy]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := ⋯
n : ℕ
⊢ f (n + 1) +ᵥ ↑(𝓂[K] ^ n) ⊆ S n

Tactic:
simpa [S] using (hf n.le_succ).symm

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : IsCompact (Metric.closedBall 0 1)
⊢ ProperSpace K

Tactic:
suffices LocallyCompactSpace K from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace K
    exact IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup h <|
      Metric.closedBall_mem_nhds 0 zero_lt_one

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
C ε : ℝ
⊢ Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)

Tactic:
show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
C ε : ℝ
⊢ Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ((1 - 1) * 1 * C + 1 * ε))
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
this : Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s - ↑s * l) (𝓝[>] 1) (𝓝 0)
h₃ : Tendsto (fun s ↦ ↑s * l) (𝓝[>] 1) (𝓝 (1 * l))
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 (0 + 1 * l))

Tactic:
exact (this.add h₃).congr fun _ ↦ by ring

Goal state after:
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
⊢ ∏ p ∈ (f a).primeFactors \ (f b).primeFactors, p = ∏ p ∈ (f c).primeFactors \ (f d).primeFactors, p →
    (f a).primeFactors \ (f b).primeFactors = (f c).primeFactors \ (f d).primeFactors

Tactic:
← primeFactors_div_gcd (hf' _ ha) (hf' _ hb).ne_zero,

Goal state after:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
⊢ ∏ p ∈ (f a / (f a).gcd (f b)).primeFactors, p = ∏ p ∈ (f c).primeFactors \ (f d).primeFactors, p →
    (f a / (f a).gcd (f b)).primeFactors = (f c).primeFactors \ (f d).primeFactors
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ ∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖ = 1

Tactic:
suffices ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1 from Multiset.prod_eq_one (by simpa)

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s (i + 1)) = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1)

Tactic:
calc
      (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]

Goal state after: