N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 ↔
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ γ ∈ Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
rw [Gamma_mem']
case mp
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 →
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

case mpr
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1 →
    ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 ↔
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
constructor
case mp
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
case mp
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 →
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
intro h
no goals
case mp
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
simp [← SL_reduction_mod_hom_val N γ, h]
case mpr
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
case mpr
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1 →
    ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
intro h
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i : Fin 2
⊢ ∀ (j : Fin 2), ↑(↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑1 i j
case mpr
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
ext i
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i j : Fin 2
⊢ ↑(↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑1 i j
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i : Fin 2
⊢ ∀ (j : Fin 2), ↑(↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑1 i j
intro j
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i j : Fin 2
⊢ ↑(↑γ i j) = ↑1 i j
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i j : Fin 2
⊢ ↑(↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑1 i j
rw [SL_reduction_mod_hom_val N γ]
case mpr.a.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }

case mpr.a.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }

case mpr.a.tail.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }

case mpr.a.tail.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i j : Fin 2
⊢ ↑(↑γ i j) = ↑1 i j
fin_cases i <;> fin_cases j <;> simp only [h]
no goals
case mpr.a.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }

case mpr.a.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }

case mpr.a.tail.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }

case mpr.a.tail.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]