-- Mathlib/NumberTheory/Modular.lean
theorem c_eq_zero (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : g 1 0 = 0

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
⊢ False

Tactic:
let d := g' 1 1

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ ↑g 1 0 = 0

Tactic:
have hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → g' 1 0 ≠ 1 := by
  intro g' hg'
  by_contra hc
  let a := g' 0 0
  let d := g' 1 1
  have had : T ^ (-a) * g' = S * T ^ d := by
    rw [g_eq_of_c_eq_one hc]
    dsimp [a, d]
    group
  let w := T ^ (-a) • g' • z
  have h₁ : w = S • T ^ d • z := by simp only [w, ← mul_smul, had]
  replace h₁ : normSq w < 1 := h₁.symm ▸ normSq_S_smul_lt_one (one_lt_normSq_T_zpow_smul hz d)
  have h₂ : 1 < normSq w := one_lt_normSq_T_zpow_smul hg' (-a)
  linarith

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
⊢ ↑g 1 0 = 0

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑(-g) 1 0 = 1
hg : -g • z ∈ 𝒟ᵒ
⊢ False

Tactic:
exact hp hg hc

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
⊢ False

Tactic:
let w := T ^ (-a) • g' • z

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑g 1 0 = -1
⊢ ↑(-g) 1 0 = 1

Tactic:
simp [← neg_eq_iff_eq_neg.mpr hc]

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : normSq ↑w < 1
⊢ False

Tactic:
have h₂ : 1 < normSq w := one_lt_normSq_T_zpow_smul hg' (-a)

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : normSq ↑w < 1
h₂ : 1 < normSq ↑w
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
⊢ False

Tactic:
have h₁ : w = S • T ^ d • z := by simp only [w, ← mul_smul, had]

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : w = S • T ^ d • z
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : normSq ↑w < 1
h₂ : 1 < normSq ↑w
⊢ False

Tactic:
linarith

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑(-g) 1 0 = 1
⊢ False

Tactic:
replace hg : -g • z ∈ 𝒟ᵒ := (SL_neg_smul g z).symm ▸ hg

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑(-g) 1 0 = 1
hg : -g • z ∈ 𝒟ᵒ
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1

Tactic:
intro g' hg'

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
⊢ ↑g' 1 0 ≠ 1

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
⊢ ↑g 1 0 = 0

Tactic:
have hn : g 1 0 ≠ -1 := by
  intro hc
  replace hc : (-g) 1 0 = 1 := by simp [← neg_eq_iff_eq_neg.mpr hc]
  replace hg : -g • z ∈ 𝒟ᵒ := (SL_neg_smul g z).symm ▸ hg
  exact hp hg hc

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hn : ↑g 1 0 ≠ -1
⊢ ↑g 1 0 = 0

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
⊢ ↑g' 1 0 ≠ 1

Tactic:
by_contra hc

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hn : ↑g 1 0 ≠ -1
⊢ ↑g 1 0 = 0

Tactic:
specialize hp hg

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hn : ↑g 1 0 ≠ -1
hp : ↑g 1 0 ≠ 1
⊢ ↑g 1 0 = 0

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : w = S • T ^ d • z
⊢ False

Tactic:
replace h₁ : normSq w < 1 := h₁.symm ▸ normSq_S_smul_lt_one (one_lt_normSq_T_zpow_smul hz d)

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
h₁ : normSq ↑w < 1
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
⊢ False

Tactic:
let a := g' 0 0

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ T ^ (-a) * g' = S * T ^ d

Tactic:
rw [g_eq_of_c_eq_one hc]

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ T ^ (-a) * (T ^ ↑g' 0 0 * S * T ^ ↑g' 1 1) = S * T ^ d

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
⊢ ↑g 1 0 ≠ -1

Tactic:
intro hc

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑g 1 0 = -1
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
w : ℍ := T ^ (-a) • g' • z
⊢ w = S • T ^ d • z

Tactic:
simp only [w, ← mul_smul, had]

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ T ^ (-a) * (T ^ ↑g' 0 0 * S * T ^ ↑g' 1 1) = S * T ^ d

Tactic:
dsimp [a, d]

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ T ^ (-↑g' 0 0) * (T ^ ↑g' 0 0 * S * T ^ ↑g' 1 1) = S * T ^ ↑g' 1 1

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑g 1 0 = -1
⊢ False

Tactic:
replace hc : (-g) 1 0 = 1 := by simp [← neg_eq_iff_eq_neg.mpr hc]

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1
hc : ↑(-g) 1 0 = 1
⊢ False

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
hn : ↑g 1 0 ≠ -1
hp : ↑g 1 0 ≠ 1
⊢ ↑g 1 0 = 0

Tactic:
rcases Int.abs_le_one_iff.mp <| abs_c_le_one hz hg with ⟨⟩ <;> tauto

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ T ^ (-↑g' 0 0) * (T ^ ↑g' 0 0 * S * T ^ ↑g' 1 1) = S * T ^ ↑g' 1 1

Tactic:
group

Result:
no goals