-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma_mem {N} {γ : SL(2, ℤ)} : γ ∈ Gamma N ↔ (γ 0 0 : ZMod N) = 1 ∧
    (γ 0 1 : ZMod N) = 0 ∧ (γ 1 0 : ZMod N) = 0 ∧ (γ 1 1 : ZMod N) = 1

Proof state:
case mpr
N : ℕ
γ : SL(2, ℤ)
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1 →
    (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1

Tactic:
intro h

Result:
case mpr
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1

Proof state:
case mp
N : ℕ
γ : SL(2, ℤ)
⊢ (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 →
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

Tactic:
intro h

Result:
case mp
N : ℕ
γ : SL(2, ℤ)
h : (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

Proof state:
N : ℕ
γ : SL(2, ℤ)
⊢ (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 ↔
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

Tactic:
constructor

Result:
case mp
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 : ℕ
γ : SL(2, ℤ)
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1 →
    (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1

Proof state:
N : ℕ
γ : SL(2, ℤ)
⊢ γ ∈ Γ(N) ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

Tactic:
rw [Gamma_mem']

Result:
N : ℕ
γ : SL(2, ℤ)
⊢ (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 ↔
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

Proof state:
case mpr.a
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

Tactic:
rw [SL_reduction_mod_hom_val N γ]

Result:
case mpr.a
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

Proof state:
case mpr.a.«0».«0»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨0, ⋯⟩ ⟨0, ⋯⟩) = ↑1 ⟨0, ⋯⟩ ⟨0, ⋯⟩

case mpr.a.«0».«1»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨0, ⋯⟩ ⟨1, ⋯⟩) = ↑1 ⟨0, ⋯⟩ ⟨1, ⋯⟩

case mpr.a.«1».«0»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨1, ⋯⟩ ⟨0, ⋯⟩) = ↑1 ⟨1, ⋯⟩ ⟨0, ⋯⟩

case mpr.a.«1».«1»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨1, ⋯⟩ ⟨1, ⋯⟩) = ↑1 ⟨1, ⋯⟩ ⟨1, ⋯⟩

Tactic:
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]

Result:
no goals

Proof state:
case mpr
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1

Tactic:
ext i j

Result:
case mpr.a
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

Proof state:
case mp
N : ℕ
γ : SL(2, ℤ)
h : (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

Tactic:
simp [← SL_reduction_mod_hom_val N γ, h]

Result:
no goals

Proof state:
case mpr.a
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

Tactic:
fin_cases i <;> fin_cases j <;> simp only [h]

Result:
case mpr.a.«0».«0»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨0, ⋯⟩ ⟨0, ⋯⟩) = ↑1 ⟨0, ⋯⟩ ⟨0, ⋯⟩

case mpr.a.«0».«1»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨0, ⋯⟩ ⟨1, ⋯⟩) = ↑1 ⟨0, ⋯⟩ ⟨1, ⋯⟩

case mpr.a.«1».«0»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨1, ⋯⟩ ⟨0, ⋯⟩) = ↑1 ⟨1, ⋯⟩ ⟨0, ⋯⟩

case mpr.a.«1».«1»
N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ ⟨1, ⋯⟩ ⟨1, ⋯⟩) = ↑1 ⟨1, ⋯⟩ ⟨1, ⋯⟩