mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x✝ : A
hx1✝ : x✝ ∈ Subring.center A
hx1 : ∀ (g : A), g * x✝ = x✝ * g
hx2 : x✝ ≠ 0
x : A
⊢ (fun x ↦ x✝ * x) (-x) = -(fun x ↦ x✝ * x) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∀ {x_1 : A}, (x_1 ∈ Set.range fun x_2 ↦ x * x_2) → -x_1 ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
a c : A
⊢ (fun x_1 ↦ x * x_1) (a * c) = a * (fun x_1 ↦ x * x_1) c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∀ {x_1 y : A}, (y ∈ Set.range fun x_2 ↦ x * x_2) → x_1 * y ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
b a : A
⊢ (fun x_1 ↦ x * x_1) (a * b) = (fun x_1 ↦ x * x_1) a * b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∀ {x_1 y : A}, (x_1 ∈ Set.range fun x_2 ↦ x * x_2) → x_1 * y ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x * 1 = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
⊢ ⟨x, hx1✝⟩ * ⟨y, ⋯⟩ = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ a * y = x * y * a * y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ x * y * a * y = y * x * a * y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * x * a * y = y * (x * a) * y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (x * a) * y = y * (a * x) * y

Tactic:
by

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
⊢ Nonempty (LocallyFiniteOrder (↥(MonoidHom.mrange v))ˣ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * x) * y = y * (a * x * y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * x * y) = y * (a * (x * y))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
⊢ MulArchimedean ↥(MonoidHom.mrange v)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * (x * y)) = y * a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : CompactSpace ↥𝒪[K]
⊢ IsPrincipalIdealRing ↥𝒪[K]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
⊢ ∀ {a : ↥(Subring.center A)}, a ≠ 0 → ∃ b, a * b = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥⊤

Tactic:
by

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

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x✝ : ∃ x, x ≠ 0 ∧ v x < 1
x : K
hx0 : x ≠ 0
hx1 : v x < 1
⊢ v ↑⟨x, ⋯⟩ < 1 ∧ ¬⟨x, ⋯⟩ = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x✝ : ∃ x, v ↑x < 1 ∧ ¬x = 0
x : ↥v.integer
hx1 : v ↑x < 1
hx0 : ¬x = 0
⊢ ↑x ≠ 0 ∧ v ↑x < 1

Tactic:
by

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
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖S t - l * ↑t‖ * t ^ (-s - 1) =
    (s - 1) * s * (Cs + ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1))

Tactic:
by

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

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsNontrivial ↔ IsLocalRing.maximalIdeal ↥v.integer ≠ ⊥

Tactic:
by

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : CompactSpace ↥𝒪[K]
this : IsDiscreteValuationRing ↥𝒪[K]
⊢ IsDiscreteValuationRing ↥𝒪[K]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: m n : ℕ
h : m < n
⊢ 2 ^ m < 2 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: ⊢ Odd (mersenne 0) ↔ 0 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
⊢ Odd (mersenne (p + 1)) ↔ p + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
⊢ mersenne (n + 1) = 2 * mersenne n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
h : Prime (mersenne p)
⊢ Prime p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
⊢ 1 ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
⊢ mersenne k + 1 = 2 ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ mersenne n % 4 = 3

Tactic:
by

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
⊢ CompactSpace ↥𝒪[K] ↔ CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
h : 3 ≤ 2 * k + 1
⊢ 1 ≤ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
odd : Odd n
h : 3 ≤ n
⊢ mersenne n % 3 = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
⊢ ProperSpace K ↔ CompactSpace ↥𝒪[K]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
h : 3 ≤ n
⊢ mersenne n % 8 = 7

Tactic:
by

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
⊢ ProperSpace K ↔ CompleteSpace K ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ mersenne p ≠ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
⊢ legendreSym (mersenne p) 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ 3 = ↑3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ 3 % 4 = 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ 2 ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ legendreSym (mersenne p) 3 = -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : p ≠ 0
i : ℕ
⊢ 0 ≤ sMod p i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p i : ℕ
⊢ sMod p i % (2 ^ p - 1) = sMod p i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i < 2 ^ p - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' i : ℕ
⊢ sZMod (p' + 2) i = ↑(s i)

Tactic:
by

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
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * (Cs + ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1)) ≤
    (s - 1) * s * C + s * ((s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ (map (castRingHom ℂ) p).mahlerMeasure

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p i : ℕ
⊢ sZMod p i = ↑(sMod p i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ ?m.28 ∣ sMod p (p - 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
⊢ p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
⊢ lucasLehmerResidue p = 0 ↔ sMod p (p - 2) = 0

Tactic:
by

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
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * C + s * ((s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1)) ≤ (s - 1) * s * C + s * ε

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y : X q
h₁ : x.1 = y.1
h₂ : x.2 = y.2
⊢ x = y

Tactic:
by

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
ε : ℝ
hε : ε > 0
⊢ ∃ C ≥ 0, (fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[𝓝[>] 1] fun s ↦ (s - 1) * s * C + s * ε

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: 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))
⊢ #(Ioo 0 n) = n - 1

Tactic:
by

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 ε : ℝ
⊢ ContinuousAt (fun s ↦ (s - 1) * s * C + s * ε) 1

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (boxPoly n B₁ B₂).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

Tactic:
by

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
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ x * y * z = x * (y * z)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x : X q
⊢ 1 * x = x

Tactic:
by

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
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)
⊢ ContinuousAt (fun s ↦ ↑s * l) 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x : X q
⊢ x * 1 = x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ↑0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ 0 ≤ 2 * ⌊↑(n.choose ↑i) * ↑B⌋ + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ 0 ≤ ↑(n.choose ↑i) * ↑B

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
⊢ {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ (↑↑n, 0) = ↑n

Tactic:
by

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
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))
x✝ : ℝ
⊢ (↑x✝ - 1) * LSeries f ↑x✝ - ↑x✝ * l + ↑x✝ * l = (↑x✝ - 1) * LSeries f ↑x✝

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ (↑(Int.negSucc n), 0) = -↑(n + 1)

Tactic:
by

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
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)
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ x * (y + z) = x * y + x * z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
⊢ {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B} ⊆
    {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ (x + y) * z = x * z + y * z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝ : X q
⊢ 0 * x✝ = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝ : X q
⊢ x✝ * 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
h_subset :
  {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B} ⊆
    {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}
⊢ {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
n m : ℤ
⊢ ↑(n * m) = ↑n * ↑m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ω * ωb = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ωb * ω = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
q : ℕ
⊢ ↑(s 0) = ω ^ 2 ^ 0 + ωb ^ 2 ^ 0

Tactic:
dsimp [s, ω, ωb]

Goal state after:
case zero
q : ℕ
⊢ ↑4 = (2, 1) ^ 1 + (2, -1) ^ 1
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
⊢ {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite ∧
    {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤ ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

Tactic:
by

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
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
⊢ n.GrahamConjecture f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this✝ : NeZero n
this : ∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖ = 1
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
by

Goal state after: