-- Mathlib/NumberTheory/Modular.lean
theorem exists_eq_T_zpow_of_c_eq_zero (hc : g 1 0 = 0) :
    ∃ n : ℤ, ∀ z : ℍ, g • z = T ^ n • z

Proof state:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ g = T ^ ↑g 0 1

Tactic:
ext i j

Result:
case h.a
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
i j : Fin 2
⊢ ↑g i j = ↑(T ^ ↑g 0 1) i j

Proof state:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∀ (z : ℍ), g • z = T ^ (-↑g 0 1) • z

Tactic:
suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]

Result:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ g = -T ^ (-↑g 0 1)

Proof state:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∀ (z : ℍ), g • z = T ^ ↑g 0 1 • z

Tactic:
suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]

Result:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ g = T ^ ↑g 0 1

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 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⟩)

Result:
case inl.intro
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

case inr.intro
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : (↑g).det = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
replace had : g 0 0 * g 1 1 = 1 := by rw [det_fin_two, hc] at had; omega

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
have had := g.det_coe

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : (↑g).det = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
⊢ g • z = T ^ ↑g 0 1 • z

Tactic:
conv_lhs => rw [this]

Result:
no goals

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : (↑g).det = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1

Tactic:
rw [det_fin_two, hc] at had

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 0 = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
⊢ ∀ (z : ℍ), g • z = T ^ ↑g 0 1 • z

Tactic:
intro z

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
⊢ g • z = T ^ ↑g 0 1 • z

Proof state:
case inl.intro
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
use g 0 1

Result:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∀ (z : ℍ), g • z = T ^ ↑g 0 1 • z

Proof state:
case h.a
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
i j : Fin 2
⊢ ↑g i j = ↑(-T ^ (-↑g 0 1)) i j

Tactic:
fin_cases i <;> fin_cases j <;>
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Result:
no goals

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
⊢ g • z = T ^ (-↑g 0 1) • z

Tactic:
conv_lhs => rw [this, SL_neg_smul]

Result:
no goals

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 0 = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1

Tactic:
omega

Result:
no goals

Proof state:
case inr.intro
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
use -(g 0 1)

Result:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∀ (z : ℍ), g • z = T ^ (-↑g 0 1) • z

Proof state:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ g = -T ^ (-↑g 0 1)

Tactic:
ext i j

Result:
case h.a
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
i j : Fin 2
⊢ ↑g i j = ↑(-T ^ (-↑g 0 1)) i j

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
⊢ ∀ (z : ℍ), g • z = T ^ (-↑g 0 1) • z

Tactic:
intro z

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
⊢ g • z = T ^ (-↑g 0 1) • z

Proof state:
case h.a
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
i j : Fin 2
⊢ ↑g i j = ↑(T ^ ↑g 0 1) i j

Tactic:
fin_cases i <;> fin_cases j <;>
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Result:
no goals