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

Goal state before:
pp: case refine_3
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.LeftInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

pp: case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

Tactic:
·

Goal state after:
case refine_3
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.LeftInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

Tactic:
·

Goal state after:
case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩
Module: Mathlib.NumberTheory.MahlerMeasure

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

Tactic:
·

Goal state after:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: case calc_1
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))
⊢ n = #𝒜

pp: case calc_2
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))
⊢ Set.MapsTo (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜) ↑(Ioo 0 n)

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))
⊢ Set.InjOn (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜)

Tactic:
·

Goal state after:
case calc_1
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))
⊢ n = #𝒜
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: case calc_2
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))
⊢ Set.MapsTo (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜) ↑(Ioo 0 n)

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))
⊢ Set.InjOn (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜)

Tactic:
·

Goal state after:
case calc_2
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))
⊢ Set.MapsTo (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜) ↑(Ioo 0 n)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case c0
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 : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure

pp: case h
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 : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ (map (castRingHom ℂ) p).natDegree ≤ n

Tactic:
·

Goal state after:
case c0
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 : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case h
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 : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ (map (castRingHom ℂ) p).natDegree ≤ n

Tactic:
·

Goal state after:
case h
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 : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ (map (castRingHom ℂ) p).natDegree ≤ n
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))
⊢ Set.InjOn (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜)

Tactic:
·

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))
⊢ Set.InjOn (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
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‖
⊢ 0 ≤ liminf (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1)

pp: case refine_2
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‖
⊢ limsup (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0

pp: case refine_3
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‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[>] 1) fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖

Tactic:
·

Goal state after:
case refine_1
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‖
⊢ 0 ≤ liminf (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
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‖
⊢ limsup (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0

pp: case refine_3
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‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[>] 1) fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖

Tactic:
·

Goal state after:
case refine_2
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‖
⊢ limsup (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_3
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‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[>] 1) fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖

Tactic:
·

Goal state after:
case refine_3
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‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[>] 1) fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n = 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n = 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ↑((∑ k ∈ Icc 1 x✝, f k) / ↑x✝) = (∑ k ∈ Icc 1 x✝, ↑(f k)) / ↑x✝

pp: case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun n ↦ ↑(f n)) ↑s

Tactic:
·

Goal state after:
case refine_1
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ↑((∑ k ∈ Icc 1 x✝, f k) / ↑x✝) = (∑ k ∈ Icc 1 x✝, ↑(f k)) / ↑x✝
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun n ↦ ↑(f n)) ↑s

Tactic:
·

Goal state after:
case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun n ↦ ↑(f n)) ↑s
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inl
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
h✝ : p = 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

pp: case inr
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

Tactic:
·

Goal state after:
case inl
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
h✝ : p = 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w✝ : ℕ
h✝ : q = 2 * w✝ + 1
⊢ (q + 1) / 2 = q / 2 + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case refine_1
p' : ℕ
⊢ 1 < p' + 2

pp: case refine_2
p' : ℕ
⊢ (mersenne (p' + 2)).minFac ≠ 2

Tactic:
·

Goal state after:
case refine_1
p' : ℕ
⊢ 1 < p' + 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case refine_2
p' : ℕ
⊢ (mersenne (p' + 2)).minFac ≠ 2

Tactic:
·

Goal state after:
case refine_2
p' : ℕ
⊢ (mersenne (p' + 2)).minFac ≠ 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case pp
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ Nat.Prime 2

pp: case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

pp: case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)

Tactic:
·

Goal state after:
case pp
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ Nat.Prime 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

pp: case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)

Tactic:
·

Goal state after:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

pp: case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)

Tactic:
· intro o
    have ω_pow :=
      congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) <|
        orderOf_dvd_iff_pow_eq_one.1 o
    have h : (1 : ZMod (q (p' + 2))) = -1 :=
      congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))
    have : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩
    apply ZMod.neg_one_ne_one h.symm

Goal state after:
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)

Tactic:
·

Goal state after:
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
p' : ℕ
hp' : p' = p - 2
⊢ p = p' + 2

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ
hp' : p' = p - 2
⊢ p = p' + 2

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ p' + 2 ≠ 2

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 2 ≤ p
n✝ : ℕ
a✝ : ↑(sModNat (2 ^ p - 1) n✝) = sMod p n✝
⊢ 2 > 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
this :
  ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
    [OrderTopology G] (g : G), 1 ≤ g → DiscreteTopology ↥(zpowers g)
ha : ¬1 ≤ g
⊢ DiscreteTopology ↥(zpowers g)

pp: G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha : 1 ≤ g
⊢ DiscreteTopology ↥(zpowers g)

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
this :
  ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
    [OrderTopology G] (g : G), 1 ≤ g → DiscreteTopology ↥(zpowers g)
ha : ¬1 ≤ g
⊢ DiscreteTopology ↥(zpowers g)
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inl
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
ha : 1 ≤ 1
⊢ DiscreteTopology ↥(zpowers 1)

pp: case inr
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
⊢ DiscreteTopology ↥(zpowers g)

Tactic:
·

Goal state after:
case inl
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
ha : 1 ≤ 1
⊢ DiscreteTopology ↥(zpowers 1)
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1) → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1}

pp: case inr.mpr
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1} → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1)

Tactic:
·

Goal state after:
case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1) → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1}
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr.mpr
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1} → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1)

Tactic:
·

Goal state after:
case inr.mpr
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1} → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1)
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case mp
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ (∃ g, zpowers g = H) → DiscreteTopology ↥H

pp: case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ DiscreteTopology ↥H → ∃ g, zpowers g = H

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ (∃ g, zpowers g = H) → DiscreteTopology ↥H
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ DiscreteTopology ↥H → ∃ g, zpowers g = H

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ DiscreteTopology ↥H → ∃ g, zpowers g = H
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case mp
Γ : Subgroup SL(2, ℤ)
⊢ (map (mapGL ℝ) Γ).IsArithmetic → Γ.FiniteIndex

Tactic:
·

Goal state after:
case mp
Γ : Subgroup SL(2, ℤ)
⊢ (map (mapGL ℝ) Γ).IsArithmetic → Γ.FiniteIndex
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case mpr
Γ : Subgroup SL(2, ℤ)
⊢ Γ.FiniteIndex → (map (mapGL ℝ) Γ).IsArithmetic

Tactic:
·

Goal state after:
case mpr
Γ : Subgroup SL(2, ℤ)
⊢ Γ.FiniteIndex → (map (mapGL ℝ) Γ).IsArithmetic
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mp
N : ℕ
A : ↥(Gamma0 N)
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

pp: case mpr
N : ℕ
A : ↥(Gamma0 N)
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N

Tactic:
·

Goal state after:
case mp
N : ℕ
A : ↥(Gamma0 N)
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mpr
N : ℕ
A : ↥(Gamma0 N)
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N

Tactic:
·

Goal state after:
case mpr
N : ℕ
A : ↥(Gamma0 N)
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mp
N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N → ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

pp: case mpr
N : ℕ
A : SL(2, ℤ)
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0 → A ∈ Gamma1 N

Tactic:
·

Goal state after:
case mp
N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N → ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mpr
N : ℕ
A : SL(2, ℤ)
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0 → A ∈ Gamma1 N

Tactic:
·

Goal state after:
case mpr
N : ℕ
A : SL(2, ℤ)
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0 → A ∈ Gamma1 N
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case left
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (Γ ⊓ Γ').relIndex (mapGL ℝ).range ≠ 0

pp: case right
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (mapGL ℝ).range.relIndex (Γ ⊓ Γ') ≠ 0

Tactic:
·

Goal state after:
case left
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (Γ ⊓ Γ').relIndex (mapGL ℝ).range ≠ 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case right
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (mapGL ℝ).range.relIndex (Γ ⊓ Γ') ≠ 0

Tactic:
·

Goal state after:
case right
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (mapGL ℝ).range.relIndex (Γ ⊓ Γ') ≠ 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
·

Goal state after:
case inl.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}