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
hm : FiniteMultiplicity λ S'.c
this : 4 ≤ 3 * multiplicity λ S'.c
⊢ 2 ≤ multiplicity λ S'.c

Tactic:
lia

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
⊢ 1 < A

Tactic:
lia

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

Goal state before:
pp: a b : ℕ
hab : a + b = 1
⊢ a = 1 ∨ b = 1

Tactic:
lia

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

Goal state before:
pp: n : ℕ
h : n ∈ maximalIdeal ℕ
lt : 1 < n
⊢ 2 ≤ n

Tactic:
lia

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
⊢ 0 < b

Tactic:
lia

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
this : 2 ^ 2 ≤ b ^ 2
⊢ 0 < b ^ 2 - 1

Tactic:
lia

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

Goal state before:
pp: 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
this : p ≠ 1
⊢ 2 ≤ p

Tactic:
lia

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

Goal state before:
pp: P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : n ∈ maximalIdeal ℕ
p : ℕ := Nat.find h0
hp : p ∈ P
hp0 : p ≠ 0
this✝ : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ), Nat.Prime p → P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
hn1 : n ≠ 0
this : n ≠ 1
⊢ 1 < n

Tactic:
lia

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

Goal state before:
pp: s : LTSeries (PrimeSpectrum ℕ)
hs : 2 < s.length
⊢ 3 < s.length + 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : ¬∃ m_1 n_1, m_1 * m + n_1 * n = k
⊢ k ≤ m * n - m - n

Tactic:
contrapose! hk

Goal state after:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
⊢ Ideal.span {↑(setGcd s)} = Ideal.span (Nat.cast '' s)

Tactic:
rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
    Ideal.span, span_singleton_generator]

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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
⊢ -a i ≤ 0

Tactic:
lia

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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this : 2 * 3 ≤ multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b) + multiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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
⊢ a i ≤ 0

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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
⊢ 0 ≤ -a i

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
x✝ : ∃ n, FrobeniusNumber n s
n : ℕ
hn : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s
⊢ n + 1 > n

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
x✝ : ∃ n, FrobeniusNumber n s
n : ℕ
hn : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s
⊢ n + 2 > n

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
this : 1 < B
⊢ 0 < B

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
⊢ b * (b ^ 2 - 1) < p

Tactic:
lia

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

Goal state before:
pp: n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 2 ≤ n + 1

Tactic:
by linarith [hn]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ m ≤ p

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ b = 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ 2 ≠ 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ m + 2 ≠ 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ 1 < 2 * (m + 2)

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ m ≤ 2 * (m + 2)

Tactic:
lia

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

Goal state before:
pp: case inr.mp.right
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) := ⋯
H : ¬P ∣ differentIdeal A B
⊢ Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.under A P) =
    IsLocalRing.maximalIdeal (Localization.AtPrime P)

Tactic:
rw [← Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx'_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (3 * S.multiplicity) ∣ (S.a + S.b) * (λ * S.y) * (λ * S.z)
this : 2 ≤ S.multiplicity
⊢ 3 * S.multiplicity = 3 * S.multiplicity - 2 + 1 + 1

Tactic:
lia

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
h : λ ^ (3 * S.multiplicity - 2 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * S.w) ^ 3
this : 2 ≤ S.multiplicity
⊢ 3 * S.multiplicity - 2 + 1 + 1 = 3 * S.multiplicity

Tactic:
lia

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
hh : λ ^ (3 * S.multiplicity - 2 + 1 + 1) * S.x * S.y * S.z = λ ^ (3 * S.multiplicity) * ↑S.u * S.w ^ 3
this : 2 ≤ S.multiplicity
⊢ 3 * S.multiplicity - 2 + 1 + 1 = 3 * S.multiplicity

Tactic:
lia

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
this : 2 ≤ S.multiplicity
⊢ (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2

Tactic:
lia

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
this : 2 ≤ S.multiplicity
⊢ 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)

Tactic:
lia

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
c : K
hc : c ≠ 0
⊢ mulHeight (c • 0) = mulHeight 0

pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
⊢ mulHeight (c • x) = mulHeight x

Tactic:
· rw [smul_zero]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
⊢ mulHeight (c • x) = mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
j : Fin n ⊕ Fin 1
i : ℕ
h : i < 1
⊢ i = 0

Tactic:
lia

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

Goal state before:
pp: case inr.inr.inr.inr
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x

Tactic:
mulHeight_eq hA,

Goal state after:
case inr.inr.inr.inr
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    ↑(Nat.card ι) ^ totalWeight K *
        ((map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) *
      mulHeight x
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
this : 2 ≤ S.multiplicity
⊢ S.multiplicity ≠ 0

Tactic:
lia

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

Goal state before:
pp: case h₂
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N

Tactic:
rw [hp.degree_eq_sum_deg_support hs₁, ← Finset.prod_pow_eq_pow_sum]
    gcongr with i
    exact Finite.le_ciSup (fun j ↦ v (x j)) i

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

Goal state before:
pp: n : ℕ
⊢ 0 < n + 1

Tactic:
lia

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
⊢ (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)

Tactic:
rw [EventuallyEq, eventually_nhdsWithin_iff]

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

Goal state before:
pp: case e_a.e_a
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ 0 = 0 + 0 * (ψ (1 - 1) - 1)

Tactic:
zero_mul,

Goal state after:
case e_a.e_a
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ 0 = 0 + 0
Module: Mathlib.NumberTheory.Height.NumberField

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

Tactic:
lia

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

Goal state before:
pp: case h₂
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 : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) * (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N

Tactic:
have := (Function.ne_iff.mp h₀).nonempty
    have F := hasFiniteMulSupport_iSup_nonarchAbsVal hx
    rw [finprod_pow F, ← finprod_mul_distrib (by fun_prop) (by fun_prop)]
    refine finprod_le_finprod (by fun_prop)
      (fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) fun v ↦ Real.iSup_le
      (fun j ↦ ?_) ?_
    · grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x]
      gcongr
      · exact HH₁ v.val
      · grw [← HH₂, ← le_max_left]
    · exact mul_nonneg (iSup_nonneg fun _ ↦ by positivity) <| by simp only [HH₁]

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
ψ : AddChar F R
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
gaussSum_mul _ _ ψ,

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
ψ : AddChar F R
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ t, ∑ x, χ x * φ (t - x) * ψ t
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
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ (∑ x ∈ univ \ {0}, (χ * φ) x * ψ x + 0 * ψ 0) * jacobiSum χ φ = (∑ i ∈ univ \ {0}, (χ * φ) i * ψ i) * jacobiSum χ φ

Tactic:
zero_mul,

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
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ (∑ x ∈ univ \ {0}, (χ * φ) x * ψ x + 0) * jacobiSum χ φ = (∑ i ∈ univ \ {0}, (χ * φ) i * ψ i) * jacobiSum χ φ
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
filter_upwards [eventually_mem_nhdsWithin,
    riemannZeta₁_ne_zero_of_near_one.filter_mono nhdsWithin_le_nhds] with s hs

Goal state after:
s : ℂ
hs : s ∈ {1}ᶜ
⊢ riemannZeta₁ s ≠ 0 → (riemannZeta s)⁻¹ = (s - 1) * (riemannZeta₁ s)⁻¹
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ 0 * (ψ (1 - 1) - 1) = 0 * (μ - 1) ^ 2

Tactic:
zero_mul,

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ 0 = 0 * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
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
⊢ ∃ z ∈ ℤ[μ], ↑(Fintype.card F) - 2 = -1 + z * (μ - 1) ^ 2

Tactic:
refine ⟨q * z₁, Subalgebra.mul_mem _ (Subalgebra.natCast_mem _ q) hz₁, ?_⟩

Goal state after:
case pos
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
⊢ ↑(Fintype.card F) - 2 = -1 + ↑q * z₁ * (μ - 1) ^ 2
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
⊢ -1 = -1 + 0 * (μ - 1) ^ 2

Tactic:
zero_mul,

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
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
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

Tactic:
zero_mul,

Goal state after:
case pos
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
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: 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
⊢ n ≠ 0

Tactic:
lia

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 : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ ({ toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) } %ₘ f).coeff ↑i = g i

Tactic:
rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff ↑i = g i

R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
⊢ 0 < orderOf χ - 1

Tactic:
lia

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
⊢ orderOf χ - 1 < orderOf χ

Tactic:
lia

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
this :
  gaussSum χ ψ ^ (orderOf χ - 1 + 1) =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ 0 < orderOf χ

Tactic:
lia

Goal state after: