mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_2
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
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hj' : c ∈ if v j ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v j}
⊢ ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i

Tactic:
use j, hj

Goal state after:
case right
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
a0 : 0 < v a
U : K → Set K := ⋯
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hj' : c ∈ if v j ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v j}
⊢ (if hi' : v j ≤ ↑↑z then z else Units.mk0 ⟨v j, ⋯⟩ ⋯) = i
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = fastLegendreSym p a

Tactic:
;

Goal state after:
p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = fastLegendreSym p a
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 y : A
⊢ (fun x ↦ x✝ * x) x + (fun x ↦ x✝ * x) y ∈ Set.range fun x ↦ x✝ * x

Tactic:
;

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
x y : A
⊢ (fun x ↦ x✝ * x) x + (fun x ↦ x✝ * x) y ∈ Set.range fun x ↦ x✝ * x
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 ∈ Set.range fun x ↦ x✝ * x

Tactic:
;

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
x : A
⊢ -(fun x ↦ x✝ * x) x ∈ Set.range fun x ↦ x✝ * x
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
⊢ a * (fun x_1 ↦ x * x_1) c ∈ Set.range fun x_1 ↦ x * x_1

Tactic:
;

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
a c : A
⊢ a * (fun x_1 ↦ x * x_1) c ∈ Set.range fun x_1 ↦ x * x_1
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
⊢ x * (a * c) = a * (x * c)

Tactic:
;

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
a c : A
⊢ x * (a * c) = a * (x * c)
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 ∈ Set.range fun x_1 ↦ x * x_1

Tactic:
;

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
b a : A
⊢ (fun x_1 ↦ x * x_1) a * b ∈ Set.range fun x_1 ↦ x * x_1
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
⊢ x * (a * b) = x * a * b

Tactic:
;

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
b a : A
⊢ x * (a * b) = x * a * b
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 := ⋯
y : A
hy : x * y = 1
⊢ ↑(⟨x, hx1✝⟩ * ⟨y, ⋯⟩) = ↑1

Tactic:
;

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.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥(Subring.center A)

Tactic:
;

Goal state after:
A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥(Subring.center A)
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
;

Goal state after:
case h
m n : ℕ
h : m < n
⊢ 1 < 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
n n✝ : ℕ
hmn✝ : 2 ≤ n✝
a✝ : mersenne n✝ % 4 = 3
⊢ (2 * mersenne n✝ + 1) % 4 = 3

Tactic:
;

Goal state after:
case succ
n n✝ : ℕ
hmn✝ : 2 ≤ n✝
a✝ : mersenne n✝ % 4 = 3
⊢ (2 * mersenne n✝ + 1) % 4 = 3
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

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

Tactic:
exact isCompact_closedBall 0 1

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
n n✝ : ℕ
hmn✝ : 3 ≤ n✝
a✝ : mersenne n✝ % 8 = 7
⊢ (2 * mersenne n✝ + 1) % 8 = 7

Tactic:
;

Goal state after:
case succ
n n✝ : ℕ
hmn✝ : 3 ≤ n✝
a✝ : mersenne n✝ % 8 = 7
⊢ (2 * mersenne n✝ + 1) % 8 = 7
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p' : ℕ
⊢ 4 = ↑4

Tactic:
;

Goal state after:
case zero
p' : ℕ
⊢ 4 = ↑4
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2

Tactic:
;

Goal state after:
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case mk
q : ℕ
y : X q
fst✝ snd✝ : ZMod q
h₁ : (fst✝, snd✝).1 = y.1
h₂ : (fst✝, snd✝).2 = y.2
⊢ (fst✝, snd✝) = y

Tactic:
;

Goal state after:
case mk
q : ℕ
y : X q
fst✝ snd✝ : ZMod q
h₁ : (fst✝, snd✝).1 = y.1
h₂ : (fst✝, snd✝).2 = y.2
⊢ (fst✝, snd✝) = y
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case mk.mk
q : ℕ
fst✝¹ snd✝¹ fst✝ snd✝ : ZMod q
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
;

Goal state after:
case mk.mk
q : ℕ
fst✝¹ snd✝¹ fst✝ snd✝ : ZMod q
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
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 ε : ℝ
⊢ ε = (1 - 1) * 1 * C + 1 * ε

Tactic:
;

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
C ε : ℝ
⊢ ε = (1 - 1) * 1 * C + 1 * ε
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)
⊢ l = 0 + 1 * l

Tactic:
;

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₁ : ∀ {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)
⊢ l = 0 + 1 * l
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₁
q : ℕ
⊢ 2 * 2 + -3 = 1

Tactic:
;

Goal state after:
case h₁
q : ℕ
⊢ 2 * 2 + -3 = 1
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:
;

Goal state after:
q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 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 →+* ℂ
x✝ : ℤ
⊢ ((algebraMap ℤ ℂ).comp (RingHom.id ℤ)) x✝ = (ψ.comp (algebraMap ℤ ↥K)) x✝

Tactic:
;

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: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (2 * ω) ^ ((q + 1) / 2) = -2

Tactic:
rw [← one_add_α_sq, ← pow_mul]
  have : 2 * ((q + 1) / 2) = q + 1 := by
    apply Nat.mul_div_cancel'
    rw [← even_iff_two_dvd]
    exact Odd.add_one odd
  rw [this, one_add_α_pow_q_succ odd leg3]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 * ω ^ ((q + 1) / 2) = -2
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ ω ^ ((q + 1) / 2) = -1

Tactic:
(by ring : (-2 : X q) = 2 * -1)

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 * ω ^ ((q + 1) / 2) = 2 * -1
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ ω ^ ((q + 1) / 2) = -1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
this : ω ^ ((q + 1) / 2) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
k : ℕ
hk : q + 1 = 4 * k
⊢ (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4

Tactic:
;

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
this : ω ^ ((q + 1) / 2) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
k : ℕ
hk : q + 1 = 4 * k
⊢ (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
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)
Γ : Subgroup (SL n R)
g : SL n R
hg : g ∈ ↑Γ
⊢ GeneralLinearGroup.det (toGL g) = 1

Tactic:
;

Goal state after:
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : CommRing R
Γ✝ : Subgroup (GL n R)
Γ : Subgroup (SL n R)
g : SL n R
hg : g ∈ ↑Γ
⊢ GeneralLinearGroup.det (toGL 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)
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
Γ : Subgroup (SL n R)
g : SL n R
hg : g ∈ ↑Γ
⊢ GeneralLinearGroup.det ((mapGL S) g) = 1

Tactic:
;

Goal state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
R : Type u_2
inst✝² : CommRing R
Γ✝ : Subgroup (GL n R)
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
Γ : Subgroup (SL n R)
g : SL n R
hg : g ∈ ↑Γ
⊢ GeneralLinearGroup.det ((mapGL S) 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)
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : SL n R
⊢ GeneralLinearGroup.det ((mapGL S) g) = 1

Tactic:
;

Goal state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
R : Type u_2
inst✝² : CommRing R
Γ : Subgroup (GL n R)
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : SL n R
⊢ GeneralLinearGroup.det ((mapGL S) g) = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
hv : 0 • ↑⟨w, hw⟩ ≠ 0
⊢ False

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
hv : 0 • ↑⟨w, hw⟩ ≠ 0
⊢ False
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

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

Tactic:
convert! (HasDetPlusMinusOne.det_eq hg).symm using 1 <;>
        simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

Goal state after:
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, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    (↑A₂.den)⁻¹ • ↑(a₁ * a₂ * M) • (↑A₁.den)⁻¹ • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)

Tactic:
← mul_smul,

Goal state after:
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, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    ((↑A₂.den)⁻¹ * ↑(a₁ * a₂ * M)) • (↑A₁.den)⁻¹ • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)
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, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    ((↑A₂.den)⁻¹ * ↑(a₁ * a₂ * M)) • (↑A₁.den)⁻¹ • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)

Tactic:
← mul_smul,

Goal state after:
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, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    ((↑A₂.den)⁻¹ * ↑(a₁ * a₂ * M) * (↑A₁.den)⁻¹) • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)
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
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
⊢ (↑g 1 1 - ↑g 0 0) ^ 2 - 4 * ↑g 1 0 * -↑g 0 1 = 0

Tactic:
;

Goal state after:
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
⊢ (↑g 1 1 - ↑g 0 0) ^ 2 - 4 * ↑g 1 0 * -↑g 0 1 = 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
⊢ ∃ N,
    N ≠ 0 ∧
      toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
obtain ⟨N, hN, h⟩ := exists_Gamma_le_conj g M

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
N : ℕ
hN : N ≠ 0
h : ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
⊢ ∃ N,
    N ≠ 0 ∧
      toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) Γ(M)
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : SlashInvariantForm Γ k
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ γ ∈ Γ, toFun✝ ∣[k] γ = toFun✝
h : { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : SlashInvariantForm Γ k
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ γ ∈ Γ, toFun✝ ∣[k] γ = toFun✝
h : { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ } = g
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toFun✝¹ : ℍ → ℂ
slash_action_eq'✝¹ : ∀ γ ∈ Γ, toFun✝¹ ∣[k] γ = toFun✝¹
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ γ ∈ Γ, toFun✝ ∣[k] γ = toFun✝
h :
  { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ }.toFun =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ } =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toFun✝¹ : ℍ → ℂ
slash_action_eq'✝¹ : ∀ γ ∈ Γ, toFun✝¹ ∣[k] γ = toFun✝¹
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ γ ∈ Γ, toFun✝ ∣[k] γ = toFun✝
h :
  { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ }.toFun =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ } =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
x✝ : ℍ
⊢ (Function.const ℍ x ∣[0] g) x✝ = Function.const ℍ x x✝

Tactic:
;

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
x✝ : ℍ
⊢ (Function.const ℍ x ∣[0] g) x✝ = Function.const ℍ x x✝
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
x✝ : Fin 2
⊢ (fun g ↦ ↑g 1) ⟨A, det_A_1⟩ x✝ = cd x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
x✝ : Fin 2
⊢ (fun g ↦ ↑g 1) ⟨A, det_A_1⟩ x✝ = cd x✝
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 0 ≤ if h : DiscreteTopology ↥𝒢.strictPeriods then |⋯.choose| else 0

Tactic:
;

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 0 ≤ if h : DiscreteTopology ↥𝒢.strictPeriods then |⋯.choose| else 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ (Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)).IsParabolic

Tactic:
rw [GeneralLinearGroup.isParabolic_iff_of_upperTriangular (by simp)]

Goal state after:
case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 0 =
      ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 1 1 ∧
    ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 1 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 0 =
      ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 1 1 ∧
    ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 1 ≠ 0

Tactic:
simpa using h.ne'

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

Goal state before:
pp: case mpr.inl
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : upperRightHom x ∈ 𝒢
hgi : ↑(upperRightHom x) 1 0 = 0
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢

Tactic:
exact ⟨x, hx, hgg⟩

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

Goal state before:
pp: case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
⊢ (∃ x_1, (↑(↑x_1 0 0) = 1 ∧ ↑(↑x_1 0 1) = 0 ∧ ↑(↑x_1 1 0) = 0 ∧ ↑(↑x_1 1 1) = 1) ∧ (mapGL ℝ) x_1 = upperRightHom x) →
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)

pp: case mpr
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N) →
    ∃ x_1, (↑(↑x_1 0 0) = 1 ∧ ↑(↑x_1 0 1) = 0 ∧ ↑(↑x_1 1 0) = 0 ∧ ↑(↑x_1 1 1) = 1) ∧ (mapGL ℝ) x_1 = upperRightHom x

Tactic:
· rintro ⟨g, ⟨-, hg, -, -⟩, hx⟩
    rw [show x = g 0 1 by simpa using congr_arg (· 0 1) hx.symm]
    apply AddSubgroup.mem_map_of_mem
    rwa [Int.mem_zmultiples_iff, ← ZMod.intCast_zmod_eq_zero_iff_dvd]

Goal state after:
case mpr
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N) →
    ∃ x_1, (↑(↑x_1 0 0) = 1 ∧ ↑(↑x_1 0 1) = 0 ∧ ↑(↑x_1 1 0) = 0 ∧ ↑(↑x_1 1 1) = 1) ∧ (mapGL ℝ) x_1 = upperRightHom x
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ 0 < ↑(Matrix.GeneralLinearGroup.det (J * g))

Tactic:
by simpa using hg

Goal state after: