awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
n : ℤ
rw : (↑(T ^ n • z) : ℂ).im = z.im
rw₁ : ((↑z : ℂ) + (↑n : ℂ)).im = z.im
rw₂ : (↑z : ℂ).im + Complex.im (↑n : ℂ) = z.im
rw₃ : (↑z : ℂ).im + 0 = z.im
rw₄ : (↑z : ℂ).im = z.im
⊢ (T ^ n • z).im = z.im
have rw₅ : z.im = z.im
Tactic: rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
have had : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
Tactic: have had := g.det_coe
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
have had₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * 0 = 1
Tactic: rw [det_fin_two, hc] at had
Cleared hypotheses: had
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
had : (↑g : Matrix (Fin 2) (Fin 2) ℤ).det = 1
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
have had₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1
Tactic: replace had : g 0 0 * g 1 1 = 1 := by rw [det_fin_two, hc] at had; lia
Cleared hypotheses: had
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
have 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
Tactic: rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
have 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
Tactic: rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
have h : ∀ (z : ℍ), g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
Tactic: use g 0 1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℍ
| g • z
have rw : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℍ
⊢ g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
have conv_lhs : g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
have conv_lhs₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ ∀ (z : ℍ), g • z = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 • z
have h : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
Tactic: suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) i j
have h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j =
  (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) i j
have h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑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
have h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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, ⋯⟩)
⊢ (↑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
have h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑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
have h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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, ⋯⟩)
⊢ (↑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
have h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ ∃ (n : ℤ), ∀ (z : ℍ), g • z = T ^ n • z
have h : ∀ (z : ℍ), g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
Tactic: use -(g 0 1)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℍ
| g • z
have rw : T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
Tactic: rw [this, SL_neg_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℍ
⊢ g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
have conv_lhs : g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
Tactic: conv_lhs => rw [this, SL_neg_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
have conv_lhs₁ : T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
Tactic: conv_lhs => rw [this, SL_neg_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ ∀ (z : ℍ), g • z = T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) • z
have h : g = -T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
Tactic: suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 = -T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) i j
have h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j =
  (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) i j
have h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑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
have h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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, ⋯⟩)
⊢ (↑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
have h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑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
have h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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, ⋯⟩)
⊢ (↑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
have h₁ : (↑g : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑(-T ^ (-(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
have hg : 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ).det
Tactic: have hg := g.det_coe.symm
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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
have 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
Tactic: rw [det_fin_two, hc] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hg : 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ).det
⊢ g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1
have 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
Tactic: replace hg : g 0 1 = g 0 0 * g 1 1 - 1 := by rw [det_fin_two, hc] at hg; lia
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have 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) ℤ)
Tactic: refine Subtype.ext ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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) ℤ)
have 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) ℤ)
Tactic: rw [(g : Matrix _ _ ℤ).eta_fin_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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) ℤ) =
    (↑(T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) :
      Matrix (Fin 2) (Fin 2) ℤ)
have 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) ℤ)
Tactic: conv_lhs => rw [(g : Matrix _ _ ℤ).eta_fin_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
h : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑(S • z) : ℂ) : ℝ) (1 : ℝ)
have 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 : ℝ)
Tactic: rw [UpperHalfPlane.coe_specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ z.im < (S • z).im
have 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 : ℂ)) :
      ℝ)
Tactic: rw [ModularGroup.im_smul_eq_div_normSq]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
⊢ z.im < HDiv.hDiv (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
have imz : 0 < z.im
Tactic: have imz : 0 < z.im := im_pos z
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
z : ℍ
h : LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
imz : 0 < z.im
⊢ z.im < HDiv.hDiv (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
have apply : HMul.hMul (β := ℝ) z.im ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) < z.im
Tactic: apply (lt_div_iff₀ z.normSq_pos).mpr