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

Goal state before:
pp: case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : a % ↑b = 0
⊢ J(0 | b) = 0

Tactic:
zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))

Goal state after:
case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : a % ↑b = 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a % ↑b | b) = J(↑(a % ↑b).natAbs | b)

pp: case neg.hb2
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b % 2 = 1

pp: case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1

Tactic:
Int.natAbs_of_nonneg (a.emod_nonneg (mod_cast hb0))

Goal state after:
case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a % ↑b | b) = J(a % ↑b | b)

case neg.hb2
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b % 2 = 1

case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1
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
⊢ ProperSpace K → IsCompact (Metric.closedBall 0 1)

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

Tactic:
<;>

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: case zero
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ sMod p 0

pp: case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ sMod p (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ sMod p 0

case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ sMod p (n✝ + 1)
Module: Mathlib.NumberTheory.LucasLehmer

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

pp: case succ
p n✝ : ℕ
⊢ sMod p (n✝ + 1) % (2 ^ p - 1) = sMod p (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ sMod p 0 % (2 ^ p - 1) = sMod p 0

case succ
p n✝ : ℕ
⊢ sMod p (n✝ + 1) % (2 ^ p - 1) = sMod p (n✝ + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p : ℕ
⊢ sZMod p 0 = ↑(sMod p 0)

pp: case succ
p n✝ : ℕ
a✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ sZMod p (n✝ + 1) = ↑(sMod p (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ sZMod p 0 = ↑(sMod p 0)

case succ
p n✝ : ℕ
a✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ sZMod p (n✝ + 1) = ↑(sMod p (n✝ + 1))
Module: Mathlib.NumberTheory.LucasLehmer

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

pp: case succ
p n✝ : ℕ
a✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ ↑(sMod p n✝) ^ 2 - 2 = ↑(sMod p n✝) ^ 2 - 2

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ 4 = 4

case succ
p n✝ : ℕ
a✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ ↑(sMod p n✝) ^ 2 - 2 = ↑(sMod p n✝) ^ 2 - 2
Module: Mathlib.NumberTheory.LucasLehmer

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

pp: p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) < 2 ^ p - 1

Tactic:
<;>

Goal state after:
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ 0 ≤ sMod p (p - 2)

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

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

pp: case h₂
q : ℕ
x y z : X q
⊢ (x * y * z).2 = (x * (y * z)).2

Tactic:
<;>

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: case h₁
q : ℕ
x y z : X q
⊢ (x.1 * y.1 + 3 * x.2 * y.2) * z.1 + 3 * (x.1 * y.2 + x.2 * y.1) * z.2 =
    x.1 * (y.1 * z.1 + 3 * y.2 * z.2) + 3 * x.2 * (y.1 * z.2 + y.2 * z.1)

pp: case h₂
q : ℕ
x y z : X q
⊢ (x.1 * y.1 + 3 * x.2 * y.2) * z.2 + (x.1 * y.2 + x.2 * y.1) * z.1 =
    x.1 * (y.1 * z.2 + y.2 * z.1) + x.2 * (y.1 * z.1 + 3 * y.2 * z.2)

Tactic:
<;>

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

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

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

pp: case h₂
q : ℕ
x : X q
⊢ (1 * x).2 = x.2

Tactic:
<;>

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: case h₁
q : ℕ
x : X q
⊢ (x * 1).1 = x.1

pp: case h₂
q : ℕ
x : X q
⊢ (x * 1).2 = x.2

Tactic:
<;>

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: case h₁
q : ℕ
⊢ (↑0).1 = 0.1

pp: case h₂
q : ℕ
⊢ (↑0).2 = 0.2

Tactic:
<;>

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: case h₁
q x✝ : ℕ
⊢ (↑(x✝ + 1)).1 = (↑x✝ + 1).1

pp: case h₂
q x✝ : ℕ
⊢ (↑(x✝ + 1)).2 = (↑x✝ + 1).2

Tactic:
<;>

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: case h₁
q n : ℕ
⊢ (↑↑n, 0).1 = (↑n).1

pp: case h₂
q n : ℕ
⊢ (↑↑n, 0).2 = (↑n).2

Tactic:
<;>

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: case h₁
q n : ℕ
⊢ (↑(Int.negSucc n), 0).1 = (-↑(n + 1)).1

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

Tactic:
<;>

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: case h₁
q : ℕ
x y z : X q
⊢ (x * (y + z)).1 = (x * y + x * z).1

pp: case h₂
q : ℕ
x y z : X q
⊢ (x * (y + z)).2 = (x * y + x * z).2

Tactic:
<;>

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: case h₁
q : ℕ
x y z : X q
⊢ x.1 * (y.1 + z.1) + 3 * x.2 * (y.2 + z.2) = x.1 * y.1 + 3 * x.2 * y.2 + (x.1 * z.1 + 3 * x.2 * z.2)

pp: case h₂
q : ℕ
x y z : X q
⊢ x.1 * (y.2 + z.2) + x.2 * (y.1 + z.1) = x.1 * y.2 + x.2 * y.1 + (x.1 * z.2 + x.2 * z.1)

Tactic:
<;>

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

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

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

pp: case h₂
q : ℕ
x y z : X q
⊢ ((x + y) * z).2 = (x * z + y * z).2

Tactic:
<;>

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: case h₁
q : ℕ
x y z : X q
⊢ (x.1 + y.1) * z.1 + 3 * (x.2 + y.2) * z.2 = x.1 * z.1 + 3 * x.2 * z.2 + (y.1 * z.1 + 3 * y.2 * z.2)

pp: case h₂
q : ℕ
x y z : X q
⊢ (x.1 + y.1) * z.2 + (x.2 + y.2) * z.1 = x.1 * z.2 + x.2 * z.1 + (y.1 * z.2 + y.2 * z.1)

Tactic:
<;>

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

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

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

pp: case h₂
q : ℕ
x✝ : X q
⊢ (0 * x✝).2 = 0.2

Tactic:
<;>

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: case h₁
q : ℕ
x✝ : X q
⊢ (x✝ * 0).1 = 0.1

pp: case h₂
q : ℕ
x✝ : X q
⊢ (x✝ * 0).2 = 0.2

Tactic:
<;>

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: case h₁
q : ℕ
x✝¹ x✝ : X q
⊢ (x✝¹ * x✝).1 = (x✝ * x✝¹).1

pp: case h₂
q : ℕ
x✝¹ x✝ : X q
⊢ (x✝¹ * x✝).2 = (x✝ * x✝¹).2

Tactic:
<;>

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: case h₁
q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹.1 * x✝.1 + 3 * x✝¹.2 * x✝.2 = x✝.1 * x✝¹.1 + 3 * x✝.2 * x✝¹.2

pp: case h₂
q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹.1 * x✝.2 + x✝¹.2 * x✝.1 = x✝.1 * x✝¹.2 + x✝.2 * x✝¹.1

Tactic:
<;>

Goal state after:
case h₁
q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹.1 * x✝.1 + 3 * x✝¹.2 * x✝.2 = x✝.1 * x✝¹.1 + 3 * x✝.2 * x✝¹.2

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

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

pp: case h₂
q : ℕ
n m : ℤ
⊢ (↑(n * m)).2 = (↑n * ↑m).2

Tactic:
<;>

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: case h₁
q n : ℕ
⊢ (↑↑n).1 = (↑n).1

pp: case h₂
q n : ℕ
⊢ (↑↑n).2 = (↑n).2

Tactic:
<;>

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: case h₁
q : ℕ
⊢ ((2, 1) * (2, -1)).1 = 1.1

pp: case h₂
q : ℕ
⊢ ((2, 1) * (2, -1)).2 = 1.2

Tactic:
<;>

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.h₁
q : ℕ
⊢ (↑4).1 = ((2, 1) ^ 1 + (2, -1) ^ 1).1

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

Tactic:
<;>

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: case h₁
q : ℕ
⊢ (α ^ 2).1 = 3.1

pp: case h₂
q : ℕ
⊢ (α ^ 2).2 = 3.2

Tactic:
<;>

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 : ℕ
⊢ α ^ 2 = 3

Tactic:
ext <;> simp [α, sq]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

pp: case h₂
q : ℕ
⊢ ((1 + α) ^ 2).2 = (2 * ω).2

Tactic:
<;>

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

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

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

pp: case h₂
q : ℕ
⊢ 1 + 1 = 2

Tactic:
<;>

Goal state after:
case h₁
q : ℕ
⊢ 1 + 3 = 2 * 2

case h₂
q : ℕ
⊢ 1 + 1 = 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' + ωb ^ 2 ^ p' = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
replace h := congr_arg (fun x => ω ^ 2 ^ p' * x) h

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

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

pp: case h₂
p : ℕ
⊢ (↑(mersenne p)).2 = 0.2

Tactic:
<;>

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' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 1) = -1

Tactic:
obtain ⟨k, w⟩ := ω_pow_formula p' h

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

Goal state before:
pp: case inl
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
inst✝ : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : GeneralLinearGroup.det g = 1
⊢ |↑(GeneralLinearGroup.det g)| = 1

pp: case inr
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
inst✝ : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : GeneralLinearGroup.det g = -1
⊢ |↑(GeneralLinearGroup.det g)| = 1

Tactic:
<;>

Goal state after:
case inl
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
inst✝ : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : GeneralLinearGroup.det g = 1
⊢ |↑(GeneralLinearGroup.det g)| = 1

case inr
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
inst✝ : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : GeneralLinearGroup.det g = -1
⊢ |↑(GeneralLinearGroup.det 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:
· rintro ⟨g, rfl⟩
    infer_instance

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.CongruenceSubgroups

Goal state before:
pp: N : ℕ
γ : SL(2, ℤ)
⊢ γ ∈ Γ(N) ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

Tactic:
simp [Gamma_mem', SpecialLinearGroup.ext_iff, and_assoc]

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

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

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

Tactic:
<;>

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.ArithmeticSubgroups

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

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

Tactic:
<;>

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

case hK
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 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
hb : b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
ha : a✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

pp: case inr
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
hb : b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
ha : -a✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
<;>

Goal state after:
case 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
hb : b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
ha : a✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

case inr
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
hb : b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
ha : -a✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
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 ∈ 𝒢}

pp: case inl.inr
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 ∈ 𝒢}

pp: case inr.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 ∈ 𝒢}

pp: case inr.inr
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 ∈ 𝒢}

case inl.inr
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 ∈ 𝒢}

case inr.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 ∈ 𝒢}

case inr.inr
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 ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

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

pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : -x✝ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
<;>

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

case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : -x✝ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case e'_1
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

pp: case e'_2
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:
<;>

Goal state after:
case e'_1
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

case e'_2
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
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun i ↦ i) ⟨0, ⋯⟩) = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun i ↦ i) ⟨1, ⋯⟩) = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun i ↦ i) ⟨0, ⋯⟩) = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun i ↦ i) ⟨1, ⋯⟩) = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case e'_1
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

pp: case e'_2
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:
<;>

Goal state after:
case e'_1
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

case e'_2
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