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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ 1 < ↑(↑x).re

Tactic:
by norm_cast

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

Goal state before:
pp: case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (fun n ↦ ‖↑↑n ^ (-s)‖ * ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun x ↦ 1

Tactic:
refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow _ _ _ ?_ hO h₂).congr_right (by simp)

Goal state after:
case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (fun n ↦ ‖↑↑n ^ (-s)‖) =O[atTop] fun n ↦ ↑n ^ (-s).re
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

Tactic:
ext1 s
  exact LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
    h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
⊢ 1 ≤ ↑n

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case a
k : ℕ
hk : k ≠ 0
| 2

Tactic:
· rw [← pow_one (2 : ℝ)]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1

Tactic:
constructor

Goal state after:
case left
⊢ 0 ≤ 1 / 4

case right
⊢ 1 / 4 ≤ 1
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ p / 2 < p

Tactic:
exact Nat.div_lt_self hp.1.pos (by decide)

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) →
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R) →
    Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ ↑↑a = ↑a

Tactic:
by norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
⊢ x ∈ I ↔ x * ϖ ^ n ∈ I * I ^ n

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := ⋯
ϖ : R := ⋯
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := ⋯
x : R
⊢ x ∈ I → x * ϖ ^ n ∈ I * I ^ n

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := ⋯
ϖ : R := ⋯
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := ⋯
x : R
⊢ x * ϖ ^ n ∈ I * I ^ n → x ∈ I
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case e'_2.e'_6
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ J(↑1 | a) = 1

pp: case e'_3
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ qrSign 1 a = 1

Tactic:
all_goals apply one_left

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
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ TotallyBounded Set.univ ↔ Finite 𝓀[K]

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ TotallyBounded Set.univ → Finite 𝓀[K]

case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ Finite 𝓀[K] → TotallyBounded Set.univ
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(χ₄ ↑b | a') = J(χ₄ ↑(b % (4 * a)) | a')

Tactic:
χ₄_nat_mod_four,

Goal state after:
case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(χ₄ ↑(b % 4) | a') = J(χ₄ ↑(b % (4 * a)) | a')
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
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
n : ℕ
hn : ‖↑p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ {y | v ↑y ≤ v ↑p ^ n} = Metric.closedBall 0 (‖p‖ ^ n)

Tactic:
ext

Goal state after:
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
n : ℕ
hn : ‖↑p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
x✝ : ↥𝒪[K]
⊢ x✝ ∈ {y | v ↑y ≤ v ↑p ^ n} ↔ x✝ ∈ Metric.closedBall 0 (‖p‖ ^ n)
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 (MonoidWithZeroHom.ofClass v)))ˣ)

Tactic:
constructor

Goal state after:
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
⊢ LocallyFiniteOrder (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
hb' : Odd (b % (4 * a.natAbs))
⊢ χ₄ ↑b * J(↑a.natAbs | b % (4 * a.natAbs)) = χ₄ ↑(b % (4 * a.natAbs)) * J(↑a.natAbs | b % (4 * a.natAbs))

Tactic:
χ₄_nat_mod_four,

Goal state after:
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
hb' : Odd (b % (4 * a.natAbs))
⊢ χ₄ ↑(b % 4) * J(↑a.natAbs | b % (4 * a.natAbs)) = χ₄ ↑(b % (4 * a.natAbs)) * J(↑a.natAbs | b % (4 * a.natAbs))
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:
ext

Goal state after:
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 := ⋯
y : A
hy : x * y = 1
⊢ ↑(⟨x, hx1✝⟩ * ⟨y, ⋯⟩) = ↑1
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 ↔ IsCompact (Metric.closedBall 0 1)

Tactic:
constructor

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

case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
⊢ IsCompact (Metric.closedBall 0 1) → ProperSpace K
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ ZMod.χ₈ ↑(mersenne p) = 1

Tactic:
ZMod.χ₈_nat_eq_if_mod_eight

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ (if mersenne p % 2 = 0 then 0 else if mersenne p % 8 = 1 ∨ mersenne p % 8 = 7 then 1 else -1) = 1
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
constructor

Goal state after:
case mp
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 → sMod p (p - 2) = 0

case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x y z : X q
⊢ (x * y * z).1 = (x * (y * z)).1

case h₂
q : ℕ
x y z : X q
⊢ (x * y * z).2 = (x * (y * z)).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x : X q
⊢ (1 * x).1 = x.1

case h₂
q : ℕ
x : X q
⊢ (1 * x).2 = x.2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x : X q
⊢ (x * 1).1 = x.1

case h₂
q : ℕ
x : X q
⊢ (x * 1).2 = x.2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
⊢ (↑0).1 = 0.1

case h₂
q : ℕ
⊢ (↑0).2 = 0.2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q x✝ : ℕ
⊢ (↑(x✝ + 1)).1 = (↑x✝ + 1).1

case h₂
q x✝ : ℕ
⊢ (↑(x✝ + 1)).2 = (↑x✝ + 1).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q n : ℕ
⊢ (↑↑n, 0).1 = (↑n).1

case h₂
q n : ℕ
⊢ (↑↑n, 0).2 = (↑n).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q n : ℕ
⊢ (↑(Int.negSucc n), 0).1 = (-↑(n + 1)).1

case h₂
q n : ℕ
⊢ (↑(Int.negSucc n), 0).2 = (-↑(n + 1)).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x y z : X q
⊢ (x * (y + z)).1 = (x * y + x * z).1

case h₂
q : ℕ
x y z : X q
⊢ (x * (y + z)).2 = (x * y + x * z).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x y z : X q
⊢ ((x + y) * z).1 = (x * z + y * z).1

case h₂
q : ℕ
x y z : X q
⊢ ((x + y) * z).2 = (x * z + y * z).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x✝ : X q
⊢ (0 * x✝).1 = 0.1

case h₂
q : ℕ
x✝ : X q
⊢ (0 * x✝).2 = 0.2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x✝ : X q
⊢ (x✝ * 0).1 = 0.1

case h₂
q : ℕ
x✝ : X q
⊢ (x✝ * 0).2 = 0.2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
x✝¹ x✝ : X q
⊢ (x✝¹ * x✝).1 = (x✝ * x✝¹).1

case h₂
q : ℕ
x✝¹ x✝ : X q
⊢ (x✝¹ * x✝).2 = (x✝ * x✝¹).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q : ℕ
n m : ℤ
⊢ (↑(n * m)).1 = (↑n * ↑m).1

case h₂
q : ℕ
n m : ℤ
⊢ (↑(n * m)).2 = (↑n * ↑m).2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
ext

Goal state after:
case h₁
q n : ℕ
⊢ (↑↑n).1 = (↑n).1

case h₂
q n : ℕ
⊢ (↑↑n).2 = (↑n).2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ (2, 1) * (2, -1) = 1

Tactic:
ext

Goal state after:
case h₁
q : ℕ
⊢ ((2, 1) * (2, -1)).1 = 1.1

case h₂
q : ℕ
⊢ ((2, 1) * (2, -1)).2 = 1.2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
q : ℕ
⊢ ↑4 = (2, 1) ^ 1 + (2, -1) ^ 1

Tactic:
ext

Goal state after:
case zero.h₁
q : ℕ
⊢ (↑4).1 = ((2, 1) ^ 1 + (2, -1) ^ 1).1

case zero.h₂
q : ℕ
⊢ (↑4).2 = ((2, 1) ^ 1 + (2, -1) ^ 1).2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ α ^ 2 = 3

Tactic:
ext

Goal state after:
case h₁
q : ℕ
⊢ (α ^ 2).1 = 3.1

case h₂
q : ℕ
⊢ (α ^ 2).2 = 3.2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ (1 + α) ^ 2 = 2 * ω

Tactic:
ext

Goal state after:
case h₁
q : ℕ
⊢ ((1 + α) ^ 2).1 = (2 * ω).1

case h₂
q : ℕ
⊢ ((1 + α) ^ 2).2 = (2 * ω).2
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
⊢ (algebraMap ℤ ℂ).comp (RingHom.id ℤ) = ψ.comp (algebraMap ℤ ↥K)

Tactic:
ext

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
x✝ : ℤ
⊢ ((algebraMap ℤ ℂ).comp (RingHom.id ℤ)) x✝ = (ψ.comp (algebraMap ℤ ↥K)) x✝
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case e'_4
q : ℕ
inst✝ : NeZero q
w : 1 < q
this : Fact (1 < q)
⊢ q ^ 2 = Fintype.card (X q)

Tactic:
rw [card_eq]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
⊢ ↑(mersenne p) = 0

Tactic:
ext

Goal state after:
case h₁
p : ℕ
⊢ (↑(mersenne p)).1 = 0.1

case h₂
p : ℕ
⊢ (↑(mersenne p)).2 = 0.2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
⊢ LucasLehmerTest p

Tactic:
by
  have : Fact (mersenne p).Prime := ⟨‹_›⟩
  set p' := p - 2 with hp'
  clear_value p'
  obtain rfl : p = p' + 2 := by lia
  dsimp [LucasLehmerTest, lucasLehmerResidue]
  rw [sZMod_eq_s p', ← X.fst_intCast, X.closed_form, add_tsub_cancel_right]
  have := X.ω_pow_trace (q := mersenne (p' + 2)) (by simp)
    (legendreSym_mersenne_three w <| hp.of_mersenne.odd_of_ne_two (by lia))
    (legendreSym_mersenne_two w) (by simp [pow_add])
  rw [succ_mersenne, pow_add, show 2 ^ 2 = 4 by norm_num, mul_div_cancel_right₀ _ (by norm_num)]
    at this
  simp [this]

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

Goal state before:
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
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1) ↔ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1}

Tactic:
constructor

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}

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

Tactic:
constructor

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

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.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:
· have := H.dense_or_cyclic
    simp only [← Subgroup.zpowers_eq_closure, Eq.comm (a := H)] at this
    refine fun hA ↦ this.elim (fun h ↦ ?_) id
    -- remains to show a contradiction assuming `H` is both dense and discrete
    obtain rfl : H = ⊤ := by
      rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]
    have : DiscreteTopology G := by rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]
    exact isCyclic_iff_exists_zpowers_eq_top.mp inferInstance

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

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

Tactic:
constructor

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

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

Goal state before:
pp: ⊢ Γ(1) = ⊤

Tactic:
ext

Goal state after:
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Γ(1) ↔ x✝ ∈ ⊤
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

Tactic:
constructor

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

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: N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
constructor

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

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: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (Γ ⊓ Γ').IsArithmetic

Tactic:
constructor

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

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

Tactic:
constructor

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

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: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ DiscreteTopology ↥(map (Int.castRingHom ℝ)).range

Tactic:
refine (Topology.IsEmbedding.toHomeomorph ?_).discreteTopology

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ Topology.IsEmbedding ⇑(map (Int.castRingHom ℝ))
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case pos
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∈ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

pp: case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
· simp [adjoinNegOne_eq_self_iff.mpr hG]

Goal state after:
case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)).FiniteIndex

Tactic:
constructor

Goal state after:
g : GL (Fin 2) ℚ
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)).index ≠ 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • (mapGL ℝ).range).IsArithmetic

Tactic:
constructor

Goal state after:
g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • (mapGL ℝ).range).Commensurable (mapGL ℝ).range
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤).Commensurable
    (Subgroup.map (mapGL ℝ) ⊤)

Tactic:
constructor

Goal state after:
case left
g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤).relIndex
      (Subgroup.map (mapGL ℝ) ⊤) ≠
    0

case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.map (mapGL ℝ) ⊤).relIndex
      (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤) ≠
    0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case right
g : GL (Fin 2) ℚ
⊢ ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) ⊤).relIndex
      ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ •
        toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤) ≠
    0

Tactic:
inv_smul_smul,

Goal state after:
case right
g : GL (Fin 2) ℚ
⊢ ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) ⊤).relIndex
      (Subgroup.map (mapGL ℝ) ⊤) ≠
    0