mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 l)

Tactic:
simpa using

Goal state after:
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
⊢ Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
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]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
⊢ 0 < v a

Tactic:
simpa using

Goal state after:
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
⊢ 0 < v a
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
hr : ¬r = 0
⊢ r ^ 2 ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
hr : ¬r = 0
⊢ ¬r = 0
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
hr1 : 1 ≤ r
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s

Tactic:
refine ⟨r', hr', hr, .trans ?_ hrs⟩
      intro x hx
      dsimp at hx ⊢
      exact hx.trans_lt (hr.trans_le hr1)

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := ⋯
n : ℕ
⊢ f (n + 1) +ᵥ ↑(𝓂[K] ^ n) ⊆ S n

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := fun n ↦ f n +ᵥ ↑(𝓂[K] ^ n)
n : ℕ
⊢ f (n + 1) ≡ f n [SMOD 𝓂[K] ^ n]
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := fun n ↦ f n +ᵥ ↑(𝓂[K] ^ n)
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
n : ℕ
y : ↥𝒪[K]
hy : y ∈ ↑(𝓂[K] ^ n)
hL : (fun x ↦ f n +ᵥ x) y ∈ ⋂ i, S i
⊢ f n ≡ (fun x ↦ f n +ᵥ x) y [SMOD 𝓂[K] ^ n • ⊤]

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := fun n ↦ f n +ᵥ ↑(𝓂[K] ^ n)
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
n : ℕ
y : ↥𝒪[K]
hy : y ∈ ↑(𝓂[K] ^ n)
hL : (fun x ↦ f n +ᵥ x) y ∈ ⋂ i, S i
⊢ y ∈ 𝓂[K] ^ n
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, hx1✝⟩ ≠ 0
⊢ x ≠ 0

Tactic:
simpa using

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, hx1✝⟩ ≠ 0
⊢ ¬x = 0
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:
simpa using

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 := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ ∃ y, x * y = x
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:
simpa using

Goal state after:
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ ?m.28 ∣ sMod p (p - 2)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_1
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑(boxPoly n B₁ B₂)
prop : ∀ (i : Fin (n + 1)), B₁ i ≤ ↑((↑p).coeff ↑i) ∧ ↑((↑p).coeff ↑i) ≤ B₂ i
⊢ (toFn (n + 1)) ↑p ∈ ↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)

Tactic:
simpa using

Goal state after:
case refine_1
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑(boxPoly n B₁ B₂)
prop : ∀ (i : Fin (n + 1)), B₁ i ≤ ↑((↑p).coeff ↑i) ∧ ↑((↑p).coeff ↑i) ≤ B₂ i
⊢ (fun x ↦ ⌈B₁ x⌉) ≤ (toFn (n + 1)) ↑p ∧ (toFn (n + 1)) ↑p ≤ fun x ↦ ⌊B₂ x⌋
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
simpa using

Goal state after:
k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
⊢ -1 = 3 ^ k
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (1 + α) ^ (q + 1) = -2

Tactic:
by
  rw [pow_succ, one_add_α_pow_q odd leg3, mul_comm, ← _root_.sq_sub_sq, α_sq]
  norm_num

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
⊢ ∃ n, 0 < n ∧ IsPrimitiveRoot z n

Tactic:
obtain ⟨_, _, hz_pow⟩ := pow_eq_one_of_mahlerMeasure_eq_one h hz₀ hz

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
w✝ : ℕ
left✝ : 0 < w✝
hz_pow : z ^ w✝ = 1
⊢ ∃ n, 0 < n ∧ IsPrimitiveRoot z n
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
⊢ ∀ (s : Set ↥H),
    (∃ a,
        IsOpen[inst✝] a ∧
          Subtype.val ⁻¹' Subtype.val ⁻¹' a =
            ⇑{ toFun := fun g ↦ ⟨↑↑g, ⋯⟩, invFun := fun g ↦ ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ } ⁻¹'
              s) ↔
      ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = s

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
⊢ ∀ (s : Set ↥H),
    (∃ a, IsOpen[inst✝] a ∧ ∀ (a_1 : G) (b : a_1 ∈ K) (b_1 : ⟨a_1, b⟩ ∈ H.subgroupOf K), a_1 ∈ a ↔ ⟨a_1, ⋯⟩ ∈ s) ↔
      ∃ t, IsOpen[inst✝] t ∧ ∀ (a : G) (b : a ∈ H), a ∈ t ↔ ⟨a, b⟩ ∈ s
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : sZMod (p' + 2) (p' + 2 - 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
sZMod_eq_s p'

Goal state after:
p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ 2 ^ (p' + 2) - 1 ∣ s p'

Tactic:
simpa using

Goal state after:
p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ 2 ^ (p' + 2) - 1 ∣ s p'
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1

Tactic:
simpa using

Goal state after:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q i : ℕ
⊢ sModNatTR q i = sModNat q i

Tactic:
rw [sModNatTR, helper, sModNatAux_eq]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sModNatTR (2 ^ p - 1) (p - 2)) = 0

Tactic:
simpa using

Goal state after:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬sModNatTR (2 ^ p - 1) (p - 2) = 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
R : Type u_2
inst✝² : CommRing R
Γ : Subgroup (GL n R)
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
h : ∀ {g : GL n R}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1
⊢ ∀ {g : GL n R}, g ∈ Γ → GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
simpa using

Goal state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
R : Type u_2
inst✝² : CommRing R
Γ : Subgroup (GL n R)
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
h : ∀ {g : GL n R}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1
⊢ ∀ {g : GL n R}, g ∈ Γ → GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 1

Tactic:
simpa using

Goal state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 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
this : Dense ↑H ∨ ∃ a, zpowers a = H
hA : DiscreteTopology ↥H
h : Dense ↑H
⊢ H = ⊤

Tactic:
by
      rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]

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

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetPlusMinusOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 1 ∨ GeneralLinearGroup.det h = -1

Tactic:
simpa using

Goal state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetPlusMinusOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 1 ∨ GeneralLinearGroup.det h = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case mp
Γ : Subgroup SL(2, ℤ)
x✝ : (map (mapGL ℝ) Γ).IsArithmetic
h : (map (mapGL ℝ) Γ).Commensurable (mapGL ℝ).range
⊢ Γ.index ≠ 0

Tactic:
simpa using

Goal state after:
case mp
Γ : Subgroup SL(2, ℤ)
x✝ : (map (mapGL ℝ) Γ).IsArithmetic
h : (map (mapGL ℝ) Γ).Commensurable (mapGL ℝ).range
⊢ ¬Γ.index = 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case mpr
Γ : Subgroup SL(2, ℤ)
x✝ : Γ.FiniteIndex
h : Γ.index ≠ 0
⊢ (map (mapGL ℝ) Γ).Commensurable (mapGL ℝ).range

Tactic:
simpa using

Goal state after:
case mpr
Γ : Subgroup SL(2, ℤ)
x✝ : Γ.FiniteIndex
h : Γ.index ≠ 0
⊢ ¬Γ.index = 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
a : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
⊢ a⁻¹ ∈ {g | ↑(↑g 1 0) = 0}

Tactic:
simpa using

Goal state after:
N : ℕ
a : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
⊢ ↑(↑a 1 0) = 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mp
N : ℕ
A : ↥(Gamma0 N)
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * ↑(↑↑A 1 1) - ↑(↑↑A 0 1) * ↑(↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Tactic:
simpa using

Goal state after:
case mp
N : ℕ
A : ↥(Gamma0 N)
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * ↑(↑↑A 1 1) - ↑(↑↑A 0 1) * ↑(↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
⊢ |↑(GeneralLinearGroup.det g ^ n)| = 1

Tactic:
obtain ⟨t, ht⟩ := hgn.1

Goal state after:
n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ) t = g ^ n
⊢ |↑(GeneralLinearGroup.det g ^ n)| = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : y.map Int.cast = 1
⊢ ∃ k, y = 1 + (a₁ * a₂ * M) • k

Tactic:
use Matrix.of fun i j ↦ (y - 1) i j / (a₁ * a₂ * M)

Goal state after:
case h
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ⋯
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ⋯
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := ⋯
a₂ : ℕ := ⋯
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : y.map Int.cast = 1
⊢ y = 1 + (a₁ * a₂ * M) • of fun i j ↦ (y - 1) i j / (↑a₁ * ↑a₂ * ↑M)
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∈ 𝒢
g : GL n R
hg : g ∈ 𝒢.adjoinNegOne
h : -g ∈ 𝒢
⊢ g ∈ 𝒢

Tactic:
simpa using

Goal state after:
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∈ 𝒢
g : GL n R
hg : g ∈ 𝒢.adjoinNegOne
h : -g ∈ 𝒢
⊢ g ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1

Tactic:
simpa using

Goal state after:
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ (↑g).det = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ![↑g 0 0, ↑g 1 0] = 0
⊢ False

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ![↑g 0 0, ↑g 1 0] = 0
⊢ False
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ¬↑g 1 0 = 0
this : discrim (↑g 1 0) (↑g 1 1 - ↑g 0 0) (-↑g 0 1) = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint

Tactic:
simpa using

Goal state after:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ¬↑g 1 0 = 0
this : discrim (↑g 1 0) (↑g 1 1 - ↑g 0 0) (-↑g 0 1) = 0
⊢ ↑g 1 0 * (c * c) + (↑g 1 1 + -↑g 0 0) * c + -↑g 0 1 = 0 ↔ c = (↑g 0 0 + -↑g 1 1) / (2 * ↑g 1 0)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • ↑c = ↑c
⊢ ↑g 1 0 * (c * c) + (↑g 1 1 + -↑g 0 0) * c + -↑g 0 1 = 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • ↑c = ↑c
⊢ ↑g 1 0 * (c * c) + (↑g 1 1 + -↑g 0 0) * c + -↑g 0 1 = 0
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
h : (a ∣[k] g) ∣[k] g⁻¹ = 0 ∣[k] g⁻¹
⊢ a = 0

Tactic:
simpa using

Goal state after:
β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
h : (a ∣[k] g) ∣[k] g⁻¹ = 0 ∣[k] g⁻¹
⊢ a = 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case refine_1
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p).IsParabolic

Tactic:
simpa using

Goal state after:
case refine_1
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ p.IsParabolic
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case refine_2
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p) • g • c = g • c

Tactic:
· simp [ConjAct.toConjAct_smul, mul_smul, hpc]

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

Goal state before:
pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0

Tactic:
simpa using

Goal state after:
case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ ¬𝒢.relIndex 𝒢' = 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0

Tactic:
simpa using

Goal state after:
case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ ¬𝒢'.relIndex 𝒢 = 0
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : Tendsto (fun x ↦ ‖f x‖) atImInfty (nhds 0)
⊢ Tendsto (fun x ↦ ‖(f ∣[k] g) x‖) atImInfty (nhds 0)

Tactic:
simpa using

Goal state after:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : Tendsto (fun x ↦ ‖f x‖) atImInfty (nhds 0)
⊢ Tendsto (fun x ↦ ‖f (g • x)‖ * (|(↑g).det| ^ (k - 1) * (|↑g 1 1| ^ k)⁻¹)) atImInfty (nhds 0)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
c : OnePoint ℝ
g : SL(2, ℤ)
hgp : ((mapGL ℝ) g).IsParabolic
hgc : (mapGL ℝ) g • c = c
⊢ c ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
simpa using

Goal state after:
case mp
c : OnePoint ℝ
g : SL(2, ℤ)
hgp : ((mapGL ℝ) g).IsParabolic
hgc : (mapGL ℝ) g • c = c
⊢ ((mapGL ℝ) g).parabolicFixedPoint ∈ Set.range (OnePoint.map Rat.cast)
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsBoundedAt f k
⊢ IsBoundedAtImInfty f

Tactic:
simpa using

Goal state after:
f : ℍ → ℂ
k : ℤ
h : ∞.IsBoundedAt f k
⊢ IsBoundedAtImInfty f
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsZeroAt f k
⊢ IsZeroAtImInfty f

Tactic:
simpa using

Goal state after:
f : ℍ → ℂ
k : ℤ
h : ∞.IsZeroAt f k
⊢ IsZeroAtImInfty f
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: a✝ : SL(2, ℤ)
x✝ : ↑((mapGL ℝ) ModularGroup.T) ∈ Set.range ⇑(Matrix.scalar (Fin 2))
a : ℝ
ha : (Matrix.scalar (Fin 2)) a = ↑((mapGL ℝ) ModularGroup.T)
⊢ 0 = 1

Tactic:
simpa using

Goal state after:
a✝ : SL(2, ℤ)
x✝ : ↑((mapGL ℝ) ModularGroup.T) ∈ Set.range ⇑(Matrix.scalar (Fin 2))
a : ℝ
ha : (Matrix.scalar (Fin 2)) a = ↑((mapGL ℝ) ModularGroup.T)
⊢ False
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
this : 0 < Fintype.card ι
⊢ (∏ i, f i) ∣[k * ↑(Fintype.card ι)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i, f i ∣[k] g

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
this : 0 < Fintype.card ι
⊢ (∏ i, f i) ∣[k * ↑(Fintype.card ι)] g = |(↑g).det| ^ (↑(Fintype.card ι) - 1) • ∏ i, f i ∣[k] g
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ f (γ • z) = f z * denom γ ↑z ^ k

Tactic:
simpa using

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ f (γ • z) = f z * denom γ ↑z ^ k
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k
f : F
γ : SL(2, ℤ)
hγ : γ ∈ Γ
z : ℍ
⊢ (Matrix.SpecialLinearGroup.mapGL ℝ) γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k
f : F
γ : SL(2, ℤ)
hγ : γ ∈ Γ
z : ℍ
⊢ γ ∈ Γ