case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)
N : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
⊢ IsCongruenceSubgroup (g • Γ)
obtain ⟨N, HN⟩ := h
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ g • Γ
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)
refine' ⟨N, _⟩
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ Γ
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ g • Γ
rw [← Gamma_cong_eq_self N g, Subgroup.pointwise_smul_le_pointwise_smul_iff]
no goals
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ Γ
exact HN