awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
N : ℕ
hN : N ≠ 0
h :
  ∀ x ∈ Γ(N),
    Membership.mem (γ := Subgroup (GL (Fin 2) ℚ)) (Subgroup.map (mapGL ℚ) Γ(M))
      (HMul.hMul (β := GL (Fin 2) ℚ) g ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) x : GL (Fin 2) ℚ) * g⁻¹)
x : SL(2, ℤ)
hx : x ∈ Γ(N)
z : SL(2, ℤ)
hz : z ∈ (↑Γ(M) : Set SL(2, ℤ))
hz' :
  (mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) z =
    HMul.hMul (β := GL (Fin 2) ℚ) g ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) x : GL (Fin 2) ℚ) * g⁻¹
right :
  (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) z =
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M))
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))

Tactic:
use z, hz
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
N : ℕ
hN : N ≠ 0
h :
  ∀ x ∈ Γ(N),
    Membership.mem (γ := Subgroup (GL (Fin 2) ℚ)) (Subgroup.map (mapGL ℚ) Γ(M))
      (HMul.hMul (β := GL (Fin 2) ℚ) g ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) x : GL (Fin 2) ℚ) * g⁻¹)
x : SL(2, ℤ)
hx : x ∈ Γ(N)
z : SL(2, ℤ)
hz : z ∈ (↑Γ(M) : Set SL(2, ℤ))
hz' :
  (mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) z =
    HMul.hMul (β := GL (Fin 2) ℚ) g ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) x : GL (Fin 2) ℚ) * g⁻¹
⊢ (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) z =
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)

Tactic:
simpa only [Subtype.ext_iff, Units.ext_iff, map_mul] using
    congr_arg (GeneralLinearGroup.map (Rat.castHom ℝ)) hz'

Premises used: Units.ext_iff, Real, Matrix.GeneralLinearGroup.map, Subtype.ext_iff, congr_arg, map_mul, Rat.castHom, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
index_ne_zero : (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).FiniteIndex

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
this :
  (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
          MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0
rwa :
  index (G := SL(2, ℤ))
      (comap (mapGL ℝ)
        (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)⁻¹ :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
    0
rwa₁ :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)⁻¹ :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0
rwa₂ :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
            ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
                ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)⁻¹ :
              ConjAct (GL (Fin 2) ℝ))
            (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤) ⊓
          MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0
rwa₃ rwa₄ rwa₅ rwa₆ :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
            ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
                ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)⁻¹ :
              ConjAct (GL (Fin 2) ℝ))
            (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
          MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0

Tactic:
rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]

Premises used: MonoidHom.range_eq_map, Subgroup.inf_relIndex_right, CongruenceSubgroup.conjGL, Subgroup.index_comap
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
index_ne_zero :
  (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
          MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0

Tactic:
suffices (t • 𝒮ℒ ⊓ 𝒮ℒ).relIndex 𝒮ℒ ≠ 0 by
    rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
index_ne_zero :
  ∀ (N : ℕ) (hN : N ≠ 0)
    (hN' :
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (mapGL ℝ) Γ(N)) ≤
        Subgroup.map (mapGL ℝ) Γ(1)),
    (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
            MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
        (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
      0
⊢ (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
          MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0

Tactic:
obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g 1

Premises used: CongruenceSubgroup.exists_Gamma_le_conj', OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    Subgroup.map (mapGL ℝ) Γ(1)
⊢ HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)

Tactic:
rw [Gamma_one_top, ← MonoidHom.range_eq_map] at hN'

Premises used: MonoidHom.range_eq_map, CongruenceSubgroup.Gamma_one_top
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)
this :
  Γ(N) ≤
    comap (mapGL ℝ)
      (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
        MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ NeZero N

Tactic:
haveI _ : NeZero N := ⟨hN⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)
this :
  Γ(N) ≤
    comap (mapGL ℝ)
      (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
        MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
h : NeZero N
⊢ (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
          MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0

Tactic:
simpa only [index_comap] using (finiteIndex_of_le this).index_ne_zero

Premises used: Subgroup.FiniteIndex.index_ne_zero, Subgroup.index_comap
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)
index_ne_zero :
  Γ(N) ≤
    comap (mapGL ℝ)
      (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
        MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
          MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)).relIndex
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠
    0

Tactic:
suffices Γ(N) ≤ (t • 𝒮ℒ ⊓ 𝒮ℒ).comap (mapGL ℝ) by
    haveI _ : NeZero N := ⟨hN⟩
    simpa only [index_comap] using (finiteIndex_of_le this).index_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) :=
  ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)
k : SL(2, ℤ)
hk : k ∈ Γ(N)
⊢ Membership.mem (γ := Subgroup SL(2, ℤ))
    (comap (mapGL ℝ)
      (HSMul.hSMul (β := Subgroup (GL (Fin 2) ℝ)) t (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ⊓
        MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)))
    k

Tactic:
simpa [mem_pointwise_smul_iff_inv_smul_mem] using
    hN' <| smul_mem_pointwise_smul _ _ _ ⟨k, hk, rfl⟩

Premises used: Subgroup.mem_pointwise_smul_iff_inv_smul_mem
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
is_commensurable :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))).Commensurable
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))).IsArithmetic

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
is_commensurable :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)).Commensurable
    (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))).Commensurable
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
rw [MonoidHom.range_eq_map]

Premises used: MonoidHom.range_eq_map
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
is_commensurable :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)).relIndex
      (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤) ≠
    0
is_commensurable₁ :
  Subgroup.relIndex (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)) ≠
    0
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)).Commensurable
    (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
is_commensurable :
  Subgroup.index (G := SL(2, ℤ))
      (Subgroup.comap (mapGL ℝ)
        (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
    0
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)).relIndex
      (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤) ≠
    0

Tactic:
rw [← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]

Premises used: Subgroup.relIndex_comap, Subgroup.relIndex_top_right
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
⊢ Subgroup.index (G := SL(2, ℤ))
      (Subgroup.comap (mapGL ℝ)
        (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
    0

Tactic:
(finiteIndex_conjGL g⁻¹).index_ne_zero

Premises used: Subgroup.FiniteIndex.index_ne_zero, CongruenceSubgroup.conjGL, ConjAct
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
⊢ Subgroup.index (G := SL(2, ℤ))
      (Subgroup.comap (mapGL ℝ)
        (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
    0

Tactic:
exact (finiteIndex_conjGL g⁻¹).index_ne_zero

Premises used: Subgroup.FiniteIndex.index_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
is_commensurable :
  Subgroup.index (G := SL(2, ℤ))
      (Subgroup.comap (mapGL ℝ)
        (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
                ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
    0
⊢ Subgroup.relIndex (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)) ≠
    0

Tactic:
rw [← Subgroup.relIndex_pointwise_smul (toConjAct (g.map (Rat.castHom ℝ)))⁻¹,
      inv_smul_smul, ← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]

Premises used: Real, ConjAct.toConjAct, Matrix.GeneralLinearGroup.map, inv_smul_smul, Inv.inv, Subgroup.relIndex_comap, Rat.castHom, Subgroup.relIndex_pointwise_smul, DFunLike.coe, Subgroup.relIndex_top_right
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
⊢ Subgroup.index (G := SL(2, ℤ))
      (Subgroup.comap (mapGL ℝ)
        (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
                ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
    0

Tactic:
(finiteIndex_conjGL g).index_ne_zero

Premises used: Subgroup.FiniteIndex.index_ne_zero, CongruenceSubgroup.conjGL, ConjAct
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
⊢ Subgroup.index (G := SL(2, ℤ))
      (Subgroup.comap (mapGL ℝ)
        (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
                ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
    0

Tactic:
exact (finiteIndex_conjGL g).index_ne_zero

Premises used: Subgroup.FiniteIndex.index_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
g : GL (Fin 2) ℚ
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      𝒢).IsArithmetic

Tactic:
⟨(Subgroup.IsArithmetic.is_commensurable.conj _).trans
    (isArithmetic_conj_SL2Z g).is_commensurable⟩

Premises used: Subgroup.IsArithmetic.mk, Subgroup.IsArithmetic.is_commensurable, Subgroup.Commensurable.trans, Subgroup.Commensurable.conj
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : IsCongruenceSubgroup Γ
g : GL (Fin 2) ℚ
obtain :
  ∀ (M : ℕ) (hN : M ≠ 0) (hΓM : Γ(M) ≤ Γ),
    IsCongruenceSubgroup
      (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))

Tactic:
obtain ⟨M, hN, hΓM⟩ := hΓ
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN : M ≠ 0
hΓM : Γ(M) ≤ Γ
⊢ NeZero M

Tactic:
haveI _ : NeZero M := ⟨hN⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
obtain :
  ∀ (N : ℕ) (hN : N ≠ 0)
    (hN' :
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (mapGL ℝ) Γ(N)) ≤
        Subgroup.map (mapGL ℝ) Γ(M)),
    IsCongruenceSubgroup
      (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))

Tactic:
obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g M

Premises used: CongruenceSubgroup.exists_Gamma_le_conj'
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    Subgroup.map (mapGL ℝ) Γ(M)
⊢ Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))

Tactic:
rw [Subgroup.pointwise_smul_subset_iff] at hN'

Premises used: Subgroup.pointwise_smul_subset_iff