case intro
N✝ : ℕ
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ+
hN : Gamma ↑N ≤ H
⊢ IsCongruenceSubgroup K
N : ℕ
H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
⊢ IsCongruenceSubgroup K
obtain ⟨N, hN⟩ := h2
no goals
case intro
N✝ : ℕ
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ+
hN : Gamma ↑N ≤ H
⊢ IsCongruenceSubgroup K
refine' ⟨N, le_trans hN h⟩