awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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⁻¹)
⊢ ∃ (N : ℕ),
    N ≠ 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 (mapGL ℝ) Γ(N)) ≤
        Subgroup.map (mapGL ℝ) Γ(M)
have refine : ∀ (y : GL (Fin 2) ℝ)
  (hy :
    y ∈
      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))),
  Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M)) y
Tactic: refine ⟨N, hN, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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⁻¹)
y : GL (Fin 2) ℝ
hy :
  y ∈
    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))
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M)) y
have hy₁ : ∃ x ∈ Γ(N),
  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) ℝ) =
    y
Tactic: simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, Subgroup.mem_map,
    eq_inv_smul_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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⁻¹)
y : GL (Fin 2) ℝ
hy :
  ∃ x ∈ Γ(N),
    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) ℝ) =
      y
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M)) y
have obtain : ∀ (x : SL(2, ℤ)) (hx : x ∈ Γ(N)),
  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: obtain ⟨x, hx, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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)
⊢ 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) ℝ))
have obtain : ∀ (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⁻¹),
  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: obtain ⟨z, hz, hz'⟩ := h x hx
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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⁻¹
⊢ 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) ℝ))
have 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) ℝ)
Tactic: use z, hz
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).FiniteIndex
have index_ne_zero : (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0
have 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
Tactic: rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0
have 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
Tactic: rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0
have 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
Tactic: rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0
have 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
Tactic: rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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))⁻¹
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)).index ≠ 0
have 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
Tactic: suffices (t • 𝒮ℒ ⊓ 𝒮ℒ).relIndex 𝒮ℒ ≠ 0 by
    rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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))⁻¹
⊢ (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
have 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
Tactic: obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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 (β := 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
have 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 ℝ)
Tactic: rw [Gamma_one_top, ← MonoidHom.range_eq_map] at hN'
Cleared hypotheses: hN'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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 ℝ))
⊢ (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
have x : NeZero N
Tactic: haveI _ : NeZero N := ⟨hN⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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 ℝ)
⊢ (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
have 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 ℝ))
Tactic: suffices Γ(N) ≤ (t • 𝒮ℒ ⊓ 𝒮ℒ).comap (mapGL ℝ) by
    haveI _ : NeZero N := ⟨hN⟩
    simpa only [index_comap] using (finiteIndex_of_le this).index_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
⊢ (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
have 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 ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
⊢ (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 ℝ))
have 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 ℝ) ⊤)
Tactic: rw [MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
⊢ (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 ℝ) ⊤)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ (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 ℝ) ⊤)
have 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
Tactic: constructor