[GOAL]
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ γ ∈ Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
[PROOFSTEP]
rw [Gamma_mem']
[GOAL]
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 ↔
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro h
[GOAL]
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
[PROOFSTEP]
simp [← SL_reduction_mod_hom_val N γ, h]
[GOAL]
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
[PROOFSTEP]
intro h
[GOAL]
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
[PROOFSTEP]
ext i j
[GOAL]
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
[PROOFSTEP]
rw [SL_reduction_mod_hom_val N γ]
[GOAL]
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
[PROOFSTEP]
fin_cases i
[GOAL]
case mpr.a.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
j : Fin 2
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } j) = ↑1 { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case mpr.a.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
j : Fin 2
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } j) = ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
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) }
[PROOFSTEP]
simp only [h]
[GOAL]
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) }
[PROOFSTEP]
simp only [h]
[GOAL]
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) }
[PROOFSTEP]
simp only [h]
[GOAL]
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) }
[PROOFSTEP]
simp only [h]
[GOAL]
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) }
[PROOFSTEP]
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]
[GOAL]
N : ℕ
⊢ Gamma 1 = ⊤
[PROOFSTEP]
ext
[GOAL]
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Gamma 1 ↔ x✝ ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
N : ℕ
⊢ Gamma 0 = ⊥
[PROOFSTEP]
ext
[GOAL]
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Gamma 0 ↔ x✝ ∈ ⊥
[PROOFSTEP]
simp only [Gamma_mem, coe_matrix_coe, Int.coe_castRingHom, map_apply, Int.cast_id, Subgroup.mem_bot]
[GOAL]
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 ↔ x✝ = 1
[PROOFSTEP]
constructor
[GOAL]
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 → x✝ = 1
[PROOFSTEP]
intro h
[GOAL]
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ x✝ = 1
[PROOFSTEP]
ext i j
[GOAL]
case h.mp.a
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
i j : Fin 2
⊢ ↑x✝ i j = ↑1 i j
[PROOFSTEP]
fin_cases i
[GOAL]
case h.mp.a.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
j : Fin 2
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } j = ↑1 { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.mp.a.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
j : Fin 2
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } j = ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.mp.a.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { 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) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.tail.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { 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) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.tail.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { 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) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
case h.mp.a.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { 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 h.mp.a.tail.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { 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 h.mp.a.tail.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { 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) }
[PROOFSTEP]
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]
[GOAL]
case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ = 1 → ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
h : x✝ = 1
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
[PROOFSTEP]
simp [h]
[GOAL]
N✝ N : ℕ
⊢ ∀ {a b : SL(2, ℤ)}, a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}
[PROOFSTEP]
intro a b ha hb
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
⊢ a * b ∈ {g | ↑(↑g 1 0) = 0}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
⊢ ↑(↑(a * b) 1 0) = 0
[PROOFSTEP]
have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
h : (↑a * ↑b) 1 0 = ↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0
⊢ ↑(↑(a * b) 1 0) = 0
[PROOFSTEP]
simp only [coe_matrix_coe, coe_mul, Int.coe_castRingHom, map_apply, Set.mem_setOf_eq] at *
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : ↑(↑a 1 0) = 0
hb : ↑(↑b 1 0) = 0
h : (↑a * ↑b) 1 0 = ↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0
⊢ ↑((↑a * ↑b) 1 0) = 0
[PROOFSTEP]
rw [h]
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : ↑(↑a 1 0) = 0
hb : ↑(↑b 1 0) = 0
h : (↑a * ↑b) 1 0 = ↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0
⊢ ↑(↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0) = 0
[PROOFSTEP]
simp [ha, hb]
[GOAL]
N✝ N : ℕ
⊢ 1 ∈
    { carrier := {g | ↑(↑g 1 0) = 0},
        mul_mem' :=
          (_ :
            ∀ {a b : SL(2, ℤ)},
              a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) }.carrier
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
⊢ ∀ {x : SL(2, ℤ)},
    x ∈
        {
              toSubsemigroup :=
                { carrier := {g | ↑(↑g 1 0) = 0},
                  mul_mem' :=
                    (_ :
                      ∀ {a b : SL(2, ℤ)},
                        a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
              one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier →
      x⁻¹ ∈
        {
              toSubsemigroup :=
                { carrier := {g | ↑(↑g 1 0) = 0},
                  mul_mem' :=
                    (_ :
                      ∀ {a b : SL(2, ℤ)},
                        a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
              one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
[PROOFSTEP]
intro a ha
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
⊢ a⁻¹ ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
⊢ ↑(↑a⁻¹ 1 0) = 0
[PROOFSTEP]
rw [SL2_inv_expl a]
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
⊢ ↑(↑{ val := ![![↑a 1 1, -↑a 0 1], ![-↑a 1 0, ↑a 0 0]],
            property := (_ : det ![![↑a 1 1, -↑a 0 1], ![-↑a 1 0, ↑a 0 0]] = 1) }
        1 0) =
    0
[PROOFSTEP]
simp only [cons_val_zero, cons_val_one, head_cons, coe_matrix_coe, coe_mk, Int.coe_castRingHom, map_apply, Int.cast_neg,
  neg_eq_zero, Set.mem_setOf_eq] at *
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha : ↑(↑a 1 0) = 0
⊢ ↑(↑a 1 0) = 0
[PROOFSTEP]
exact ha
[GOAL]
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ ↑(det ↑↑A) = 1
[PROOFSTEP]
simp [A.1.property]
[GOAL]
N✝ N : ℕ
⊢ (fun g => ↑(↑↑g 1 1)) 1 = 1
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
⊢ ∀ (x y : { x // x ∈ Gamma0 N }),
    OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } (x * y) =
      OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } x *
        OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } y
[PROOFSTEP]
intro A B
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
⊢ OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } (A * B) =
    OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A *
      OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } B
[PROOFSTEP]
have := (two_mul_expl A.1.1 B.1.1).2.2.2
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
⊢ OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } (A * B) =
    OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A *
      OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } B
[PROOFSTEP]
simp only [Subgroup.coe_mul, coe_matrix_coe, coe_mul, Int.coe_castRingHom, map_apply] at *
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
⊢ ↑((↑↑A * ↑↑B) 1 1) = ↑(↑↑A 1 1) * ↑(↑↑B 1 1)
[PROOFSTEP]
rw [this]
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
⊢ ↑(↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1) = ↑(↑↑A 1 1) * ↑(↑↑B 1 1)
[PROOFSTEP]
have ha := A.property
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
ha : ↑A ∈ Gamma0 N
⊢ ↑(↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1) = ↑(↑↑A 1 1) * ↑(↑↑B 1 1)
[PROOFSTEP]
simp only [Int.cast_add, Int.cast_mul, add_left_eq_self, Gamma0_mem, coe_matrix_coe, Int.coe_castRingHom,
  map_apply] at *
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
ha : ↑(↑↑A 1 0) = 0
⊢ ↑(↑↑A 1 0) * ↑(↑↑B 0 1) = 0
[PROOFSTEP]
rw [ha]
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
ha : ↑(↑↑A 1 0) = 0
⊢ 0 * ↑(↑↑B 0 1) = 0
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ A ∈ Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
intro ha
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
have hA := A.property
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑A ∈ Gamma0 N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
rw [Gamma0_mem] at hA 
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
have adet := Gamma0_det N A
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(det ↑↑A) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
rw [Matrix.det_fin_two] at adet 
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(↑↑A 0 0 * ↑↑A 1 1 - ↑↑A 0 1 * ↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
simp only [Gamma0Map, coe_matrix_coe, Int.coe_castRingHom, map_apply, Gamma1_mem', MonoidHom.coe_mk, OneHom.coe_mk,
  Int.cast_sub, Int.cast_mul] at *
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * ↑(↑↑A 1 1) - ↑(↑↑A 0 1) * ↑(↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
rw [hA, ha] at adet 
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * 1 - ↑(↑↑A 0 1) * 0 = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
simp only [mul_one, mul_zero, sub_zero] at adet 
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
simp only [adet, hA, ha, eq_self_iff_true, and_self_iff]
[GOAL]
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N
[PROOFSTEP]
intro ha
[GOAL]
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ A ∈ Gamma1' N
[PROOFSTEP]
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, coe_matrix_coe, Int.coe_castRingHom, map_apply]
[GOAL]
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ ↑{ toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A = 1
[PROOFSTEP]
exact ha.2.1
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
N✝ N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N → ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
intro ha
[GOAL]
case mp
N✝ N : ℕ
A : SL(2, ℤ)
ha : A ∈ Gamma1 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
simp_rw [Gamma1, Subgroup.mem_map] at ha 
[GOAL]
case mp
N✝ N : ℕ
A : SL(2, ℤ)
ha : ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
obtain ⟨⟨x, hx⟩, hxx⟩ := ha
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx : x ∈ Gamma1' N
hxx :
  { val := x, property := hx } ∈ ⊤ ∧
    ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx } = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
rw [Gamma1_to_Gamma0_mem] at hx 
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx :
  { val := x, property := hx✝ } ∈ ⊤ ∧
    ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ } = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
simp only [Subgroup.mem_top, true_and] at hxx 
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ } = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
rw [← hxx]
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ } = A
⊢ ↑(↑(↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ }) 0
          0) =
      1 ∧
    ↑(↑(↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ }) 1
            1) =
        1 ∧
      ↑(↑(↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ })
            1 0) =
        0
[PROOFSTEP]
convert hx
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0 → A ∈ Gamma1 N
[PROOFSTEP]
intro ha
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma1 N
[PROOFSTEP]
simp_rw [Gamma1, Subgroup.mem_map]
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
[PROOFSTEP]
have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma0 N
[PROOFSTEP]
simp [ha.right.right, Gamma0_mem]
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
[PROOFSTEP]
have HA : (⟨A, hA⟩ : Gamma0 N) ∈ Gamma1' N :=
  by
  simp only [Gamma1_to_Gamma0_mem, Subgroup.coe_mk, coe_matrix_coe, Int.coe_castRingHom, map_apply]
  exact ha
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ { val := A, property := hA } ∈ Gamma1' N
[PROOFSTEP]
simp only [Gamma1_to_Gamma0_mem, Subgroup.coe_mk, coe_matrix_coe, Int.coe_castRingHom, map_apply]
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
exact ha
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : { val := A, property := hA } ∈ Gamma1' N
⊢ ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
[PROOFSTEP]
refine' ⟨(⟨(⟨A, hA⟩ : Gamma0 N), HA⟩ : (Gamma1' N : Subgroup (Gamma0 N))), _⟩
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : { val := A, property := hA } ∈ Gamma1' N
⊢ { val := { val := A, property := hA }, property := HA } ∈ ⊤ ∧
    ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N)))
        { val := { val := A, property := hA }, property := HA } =
      A
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
⊢ Gamma1 N ≤ Gamma0 N
[PROOFSTEP]
intro x HA
[GOAL]
N✝ N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N
[PROOFSTEP]
simp only [Gamma0_mem, Gamma1_mem, coe_matrix_coe, Int.coe_castRingHom, map_apply] at *
[GOAL]
N✝ N : ℕ
x : SL(2, ℤ)
HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0
⊢ ↑(↑x 1 0) = 0
[PROOFSTEP]
exact HA.2.2
[GOAL]
N : ℕ
H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
⊢ IsCongruenceSubgroup K
[PROOFSTEP]
obtain ⟨N, hN⟩ := h2
[GOAL]
case intro
N✝ : ℕ
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ+
hN : Gamma ↑N ≤ H
⊢ IsCongruenceSubgroup K
[PROOFSTEP]
refine' ⟨N, le_trans hN h⟩
[GOAL]
N✝ : ℕ
N : ℕ+
⊢ Gamma ↑N ≤ Gamma ↑N
[PROOFSTEP]
simp only [le_refl]
[GOAL]
N✝ : ℕ
N : ℕ+
⊢ IsCongruenceSubgroup (Gamma1 ↑N)
[PROOFSTEP]
refine' ⟨N, _⟩
[GOAL]
N✝ : ℕ
N : ℕ+
⊢ Gamma ↑N ≤ Gamma1 ↑N
[PROOFSTEP]
intro A hA
[GOAL]
N✝ : ℕ
N : ℕ+
A : SL(2, ℤ)
hA : A ∈ Gamma ↑N
⊢ A ∈ Gamma1 ↑N
[PROOFSTEP]
simp only [Gamma1_mem, Gamma_mem] at *
[GOAL]
N✝ : ℕ
N : ℕ+
A : SL(2, ℤ)
hA : ↑(↑A 0 0) = 1 ∧ ↑(↑A 0 1) = 0 ∧ ↑(↑A 1 0) = 0 ∧ ↑(↑A 1 1) = 1
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
simp only [hA, eq_self_iff_true, and_self_iff]
[GOAL]
N✝ N : ℕ
g : ConjAct SL(2, ℤ)
⊢ g • Gamma N = Gamma N
[PROOFSTEP]
apply Subgroup.Normal.conjAct (Gamma_normal N)
[GOAL]
N : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
⊢ IsCongruenceSubgroup (g • Γ)
[PROOFSTEP]
obtain ⟨N, HN⟩ := h
[GOAL]
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)
[PROOFSTEP]
refine' ⟨N, _⟩
[GOAL]
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ g • Γ
[PROOFSTEP]
rw [← Gamma_cong_eq_self N g, Subgroup.pointwise_smul_le_pointwise_smul_iff]
[GOAL]
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ Γ
[PROOFSTEP]
exact HN
