N✝ N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N
N✝ N : ℕ
⊢ Gamma1 N ≤ Gamma0 N
intro x HA
N✝ N : ℕ
x : SL(2, ℤ)
HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0
⊢ ↑(↑x 1 0) = 0
N✝ N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N
simp only [Gamma0_mem, Gamma1_mem, coe_matrix_coe, Int.coe_castRingHom, map_apply] at *
no goals
N✝ N : ℕ
x : SL(2, ℤ)
HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0
⊢ ↑(↑x 1 0) = 0
exact HA.2.2