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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1

Tactic:
by
  obtain ⟨y, hy⟩ := h
  have : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (η + 1))) := by
    calc _ = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (η + 1)) := by
          simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring
    _ = _ := by rw [hy]; ring
  rw [this, pow_succ]
  exact mul_dvd_mul_left _ (lambda_dvd_mul_sub_one_mul_sub_eta_add_one hζ y)

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:

Tactic:
∑ x ∈ Finset.map ⟨(n ^ ·), Nat.pow_right_injective h.two_le⟩ (range m), x
        = ∑ i ∈ range m, n ^ i := by simp
      _ = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _)
      _ ≤ (n ^ m - 1) := Nat.div_le_self (n ^ m - 1) (n - 1)
      _ < n ^ m := sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos)

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ 0 < ↑n

Tactic:
positivity

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

Goal state before:
pp: case inl.«0»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = -1

pp: case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = -1

Tactic:
· tauto

Goal state after:
case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = -1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Tactic:
revert a ha; intro a; fin_cases a
    · tauto
    · simp

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

Goal state before:
pp: case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic.2777296637._hygCtx._hyg.53.«0»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i ↦ i) ⟨0, ⋯⟩ = 0 → 1 = (fun i ↦ i) ⟨0, ⋯⟩ ^ 1

pp: case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic.2777296637._hygCtx._hyg.53.«1»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i ↦ i) ⟨1, ⋯⟩ = 0 → 1 = (fun i ↦ i) ⟨1, ⋯⟩ ^ 1

Tactic:
· tauto

Goal state after:
case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic.2777296637._hygCtx._hyg.53.«1»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i ↦ i) ⟨1, ⋯⟩ = 0 → 1 = (fun i ↦ i) ⟨1, ⋯⟩ ^ 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ FermatLastTheoremFor 3

Tactic:
fermatLastTheoremFor_iff_int

Goal state after:
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ FermatLastTheoremWith ℤ 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)

Tactic:
· have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
      simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]
      exact Eq.symm

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

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
right
    exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩

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

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : P ∣ a
⊢ P ^ 2 ∣ Ideal.map (algebraMap A B) p

Tactic:
by rw [pow_two, ha]; exact mul_dvd_mul_left _ hPa

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = -1

Tactic:
rw [← h]

Goal state after:
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = 3 ^ ((n.fermatNumber - 1) / 2)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = 0

Tactic:
rw [← h]

Goal state after:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n))
Module: Mathlib.NumberTheory.Harmonic.Int

Goal state before:
pp: n : ℕ
Hn : (Finset.range n).Nonempty
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹

Tactic:
positivity

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

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

Tactic:
positivity

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

Goal state before:
pp: case e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n + 1 ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case e_a.hy
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case e_a.ha
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

Tactic:
positivity

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

Goal state before:
pp: case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
positivity

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

Goal state before:
pp: case c0
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i)

pp: case b0
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

pp: case h₁
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((x ∘ f) i)) archAbsVal).prod ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

pp: case h₂
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
· exact finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _

Goal state after:
case b0
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

case h₁
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((x ∘ f) i)) archAbsVal).prod ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

case h₂
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (↑n ^ (-1) - (↑n + 1) ^ (-1)) = log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
rpow_neg_one,

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ((↑n)⁻¹ - (↑n + 1)⁻¹) = log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_1
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

Tactic:
positivity

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

Goal state before:
pp: case refine_2
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
positivity

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

Goal state before:
pp: N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ 0 < N + 1

Tactic:
positivity

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

Goal state before:
pp: 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 ι
⊢ 0 ≤ logHeight A + logHeight x

Tactic:
positivity

Goal state after:
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
hι : Nonempty ι
this : ↑(Nat.card ι) ^ totalWeight K ≠ 0
⊢ 0 < mulHeight fun j ↦ ∑ i, A (j, i) * x i

Tactic:
positivity

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

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ ∑ x_1 ∈ p.support, v (coeff x_1 p) * ∏ x_2 ∈ x_1.support, v (x x_2) ^ x_1 x_2 ≤
    ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N

Tactic:
refine Finset.sum_le_sum fun s hs ↦ ?_

Goal state after:
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ v (coeff s p) * ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ v (coeff s p) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) * ↑(x + 1) * s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s) * 1 * s⁻¹

Tactic:
← Finset.sum_mul,

Goal state after:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ (∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1)) * s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s) * 1 * s⁻¹
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
⊢ 0 < mulHeight (x * y)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ 0 < mulHeight₁ (x * y)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
x✝¹ : ι
x✝ : x✝¹ ∈ s
⊢ mulHeight₁ (x x✝¹) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
⊢ 0 < mulHeight₁ (∏ i ∈ s, x i)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
v : AbsoluteValue K ℝ
x✝³ : v ∈ archAbsVal
x✝² : ι'
x✝¹ : ι →₀ ℕ
x✝ : x✝¹ ∈ (p x✝²).coeff.support
⊢ 0 ≤ v ((p x✝²).coeff x✝¹)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
v : AbsoluteValue K ℝ
j : ι'
x✝ : K
⊢ 0 x✝ ≤ (fun x ↦ v x) x✝

Tactic:
positivity

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

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ HasSum (fun b ↦ term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)

Tactic:
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) s)]

Goal state after:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, term (i + 1) s) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hgf
s : ℝ
hs : 1 < s
n : ℕ
⊢ (fun x ↦ 0) n ≤ (fun x ↦ ↑x / (↑x + 1) ^ s) n

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
x✝ : ↑nonarchAbsVal
⊢ 0 ≤ max (↑x✝ (∑ a ∈ s, x a)) 1

Tactic:
positivity

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

Goal state before:
pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

Tactic:
positivity

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

Goal state before:
pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
x✝ : AbsoluteValue K ℝ
h : x✝ ∈ archAbsVal
⊢ 0 ≤ ↑(#s) * ∏ a ∈ s, max (x✝ (x a)) 1

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
x✝¹ : AbsoluteValue K ℝ
x✝ : x✝¹ ∈ archAbsVal
⊢ 0 ≤ max (x✝¹ (∑ a ∈ s, x a)) 1

Tactic:
positivity

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

Goal state before:
pp: 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
v : AbsoluteValue K ℝ
j : ι'
s : ι →₀ ℕ
⊢ 0 ≤ v ((p j).coeff s)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
x✝¹ : α
x✝ : x✝¹ ∈ s
⊢ mulHeight₁ (x x✝¹) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 < x
⊢ 0 ≤ x ^ (s + 1)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
this✝ : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0
this : ↑(#s) ^ totalWeight K ≠ 0
⊢ 0 < mulHeight₁ (∑ a ∈ s, x a)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ 0 < mulHeight₁ (x + y)

Tactic:
positivity

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

Goal state before:
pp: this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 0 ≤ ↑n + 1

Tactic:
positivity

Goal state after:
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
m : ℕ
⊢ 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)

Tactic:
positivity

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

Goal state before:
pp: this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ 0 ≤ 4 * π

Tactic:
positivity

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

Goal state before:
pp: ⊢ 0 < 4 * π

Tactic:
positivity

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

Goal state before:
pp: ⊢ 0 ≤ 4 * π

Tactic:
positivity

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ 0 ≠ π

Tactic:
positivity

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

Goal state before:
pp: 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
x✝ : ι'
⊢ 0 ≤ max (⨆ s, ↑v (coeff (↑s) (p x✝))) 1

Tactic:
positivity

Goal state after:
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
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⟨i₀, ⋯⟩
this : Nonempty { j // ↑(x j) ≠ 0 }
hI : span (Set.range x) = span (Set.range fun i ↦ x ↑i)
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
have hx₀ : (fun i ↦ (x i : K)) ≠ 0 := Function.ne_iff.mpr ⟨_, i'.prop⟩

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⟨i₀, ⋯⟩
this : Nonempty { j // ↑(x j) ≠ 0 }
hI : span (Set.range x) = span (Set.range fun i ↦ x ↑i)
hx₀ : (fun i ↦ ↑(x i)) ≠ 0
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: 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
⊢ max (mulHeightBound p) 1 > 0

Tactic:
positivity

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

Goal state before:
pp: 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
⊢ 0 < mulHeight fun j ↦ (eval x) (p j)

Tactic:
positivity

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ 0 < mulHeight x ^ M

Tactic:
positivity

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ 0 < max (mulHeightBound q) 1

Tactic:
positivity

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
h✝ : Nonempty ι'
this : 0 < Nat.card ι'
⊢ (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ > 0

Tactic:
positivity

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)) →
        C * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

Tactic:
rcases isEmpty_or_nonempty ι'
  · exact ⟨1, zero_lt_one, fun p _ h ↦ by simp [mulHeight_eval_ge_aux p h]⟩
  have : 0 < Nat.card ι' := Nat.card_pos
  exact ⟨_, by positivity, mulHeight_eval_ge hq⟩

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
this : ↑(Nat.card ι') ^ totalWeight K ≠ 0
⊢ 0 < (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N

Tactic:
positivity

Goal state after: