awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
inl :
  ∀ (ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1) (hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1),
    ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
inr :
  ∀ (ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1) (hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1),
    ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)

Premises used: Int.eq_one_or_neg_one_of_mul_eq_one'
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
h : ∀ (z : ℍ), g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
use g 0 1

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
this : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
z : ℍ
rw : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
| g • z

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
this : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
z : ℍ
conv_lhs : g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
conv_lhs₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
⊢ g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z

Tactic:
conv_lhs => rw [this]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
h : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
⊢ ∀ (z : ℍ), g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z

Tactic:
suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
h :
  ∀ (i j : Fin 2),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) i j
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
i j : Fin 2
h :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
h₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) i j

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
j : Fin 2
h :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
j : Fin 2
h :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
h : ∀ (z : ℍ), g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
use -(g 0 1)

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this : g = -T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
z : ℍ
rw : T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
| g • z

Tactic:
rw [this, SL_neg_smul]

Premises used: ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this : g = -T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
z : ℍ
conv_lhs : g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
conv_lhs₁ : T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
⊢ g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z

Tactic:
conv_lhs => rw [this, SL_neg_smul]

Premises used: ModularGroup.SL_neg_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
h : g = -T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
⊢ ∀ (z : ℍ), g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z

Tactic:
suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
h :
  ∀ (i j : Fin 2),
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j =
      (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) i j
⊢ g = -T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
i j : Fin 2
h :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
h₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) i j

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
j : Fin 2
h :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
j : Fin 2
h :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
ha : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Premises used: ModularGroup.coe_T_zpow, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
⊢ 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ).det

Tactic:
have hg := g.det_coe.symm
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ).det
⊢ 1 =
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * 1

Tactic:
rw [det_fin_two, hc] at hg

Premises used: Matrix.det_fin_two
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg :
  1 =
    (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ).det
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - 1

Tactic:
replace hg : g 0 1 = g 0 0 * g 1 1 - 1 := by rw [det_fin_two, hc] at hg; lia
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - 1
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1

Tactic:
Subtype.ext ?_

Premises used: Matrix.SpecialLinearGroup, Subtype.ext
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - 1
refine :
  (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) :
      Matrix (Fin 2) (Fin 2) ℤ)
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - 1
rw :
  (!![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1;
      (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0, (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1] :
    Matrix (Fin 2) (Fin 2) ℤ)
| (↑g : Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
rw [(g : Matrix _ _ ℤ).eta_fin_two]

Premises used: Matrix.eta_fin_two
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - 1
conv_lhs :
  !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1;
      (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0, (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1] =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) :
      Matrix (Fin 2) (Fin 2) ℤ)
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) :
      Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
conv_lhs => rw [(g : Matrix _ _ ℤ).eta_fin_two]

Premises used: Matrix.eta_fin_two
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - 1
⊢ !![(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0, (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1;
      (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0, (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1] =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) :
      Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
simp only [hg, sub_eq_add_neg, hc, coe_mul, coe_T_zpow, coe_S, mul_fin_two, mul_zero, mul_one,
    zero_add, one_mul, add_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, sub_eq_add_neg, zero_add, MulZeroClass.mul_zero, Matrix.mul_fin_two, mul_one, add_zero, ModularGroup.coe_T_zpow, ModularGroup.coe_S, Matrix.SpecialLinearGroup.coe_mul, one_mul
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
rw :
  LT.lt (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
          ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ))) :
      ℝ)
    (1 : ℝ)
⊢ LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(S • z) : ℂ) : ℝ) (1 : ℝ)

Tactic:
rw [UpperHalfPlane.coe_specialLinearGroup_apply]

Premises used: UpperHalfPlane.coe_specialLinearGroup_apply
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ LT.lt (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
          ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑S : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ))) :
      ℝ)
    (1 : ℝ)

Tactic:
simpa [coe_S, num, denom] using (inv_lt_inv₀ z.normSq_pos zero_lt_one).mpr h

Premises used: Iff.mpr, UpperHalfPlane.normSq_pos, zero_lt_one, UpperHalfPlane.denom, UpperHalfPlane.num, ModularGroup.coe_S, inv_lt_inv₀
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
rw :
  z.im <
    HDiv.hDiv (β := ℝ) z.im
      ((normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
            (↑z : ℂ)) :
        ℝ)
⊢ z.im < (S • z).im

Tactic:
rw [ModularGroup.im_smul_eq_div_normSq]

Premises used: ModularGroup.im_smul_eq_div_normSq
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ 0 < z.im

Tactic:
have imz : 0 < z.im := im_pos z
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
imz : 0 < z.im
apply : HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) < z.im
⊢ z.im < HDiv.hDiv (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)

Tactic:
apply (lt_div_iff₀ z.normSq_pos).mpr

Premises used: Iff.mpr, UpperHalfPlane.normSq_pos, lt_div_iff₀
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
imz : 0 < z.im
nlinarith :
  z.im ≤ HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) →
    z.im - HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) +
        (0 - HSub.hSub (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ) * (0 - z.im)) =
      0
⊢ HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) < z.im

Tactic:
nlinarith