awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
hz' : 0 < z.im
⊢ LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑{ coe := z, coe_im_pos := hz' : ℍ } : ℂ) : ℝ)

Tactic:
simpa [Complex.normSq_eq_norm_sq]

Premises used: Complex.normSq_eq_norm_sq
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
hz' : 0 < z.im
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y

Tactic:
exact ⟨⟨z, hz'⟩, ⟨⟨by simpa [Complex.normSq_eq_norm_sq], h2⟩, h1⟩, rfl⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
rw :
  IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} ∧
    Bornology.IsBounded (α := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ IsCompact (truncatedFundamentalDomain y)

Tactic:
rw [isEmbedding_coe.isCompact_iff, coe_truncatedFundamentalDomain,
    Metric.isCompact_iff_isClosed_bounded]

Premises used: Metric.isCompact_iff_isClosed_bounded, Topology.IsEmbedding.isCompact_iff, UpperHalfPlane.isEmbedding_coe, ModularGroup.coe_truncatedFundamentalDomain
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
left : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
right : Bornology.IsBounded (α := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} ∧
    Bornology.IsBounded (α := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
left : IsClosed (X := ℂ) fun (z : ℂ) ↦ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
apply (isClosed_le continuous_const Complex.continuous_im).inter

Premises used: continuous_const, isClosed_le, IsClosed.inter, Complex.continuous_im
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
left : IsClosed (X := ℂ) fun (z : ℂ) ↦ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖

Tactic:
apply (isClosed_le Complex.continuous_im continuous_const).inter

Premises used: continuous_const, isClosed_le, IsClosed.inter, Complex.continuous_im
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
left : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖

Tactic:
apply (isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const).inter

Premises used: Complex.continuous_re, Continuous.comp, continuous_const, isClosed_le, IsClosed.inter, continuous_abs
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖

Tactic:
isClosed_le continuous_const continuous_norm

Premises used: continuous_const, isClosed_le, continuous_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖

Tactic:
exact isClosed_le continuous_const continuous_norm

Premises used: continuous_const, isClosed_le, continuous_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
⊢ Bornology.IsBounded (α := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
(Metric.isBounded_iff_subset_closedBall 0).mpr ⟨√((1 / 2) ^ 2 + y ^ 2), fun z hz ↦ ?_⟩

Premises used: Iff.mpr, HDiv.hDiv, HPow.hPow, HAdd.hAdd, Exists.intro, Real.sqrt, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
right :
  ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z),
    Membership.mem (γ := Set ℂ) (Metric.closedBall 0 √(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)) z
⊢ Bornology.IsBounded (α := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
refine (Metric.isBounded_iff_subset_closedBall 0).mpr ⟨√((1 / 2) ^ 2 + y ^ 2), fun z hz ↦ ?_⟩

Premises used: Iff.mpr, HDiv.hDiv, HPow.hPow, HAdd.hAdd, Exists.intro, Real.sqrt, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
right : ‖z‖ ≤ √(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)
⊢ Membership.mem (γ := Set ℂ) (Metric.closedBall 0 √(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)) z

Tactic:
simp only [mem_closedBall_zero_iff]

Premises used: mem_closedBall_zero_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ 0 ≤ √(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
right : HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)) 2
⊢ ‖z‖ ≤ √(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)

Tactic:
refine le_of_sq_le_sq ?_ (by positivity)

Premises used: le_of_sq_le_sq
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ 0 ≤ HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ 0 ≤ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
right : HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)) 2

Tactic:
rw [Real.sq_sqrt (by positivity), Complex.norm_eq_sqrt_sq_add_sq, Real.sq_sqrt (by positivity)]

Premises used: Real.sq_sqrt, Complex.norm_eq_sqrt_sq_add_sq
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
right : HPow.hPow (β := ℕ) z.re 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2
right₁ : HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) y 2
⊢ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2

Tactic:
apply add_le_add

Premises used: add_le_add
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
right : |z.re| ≤ 1 / 2
⊢ HPow.hPow (β := ℕ) z.re 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2

Tactic:
rw [sq_le_sq, abs_of_pos <| one_half_pos (α := ℝ)]

Premises used: sq_le_sq, one_half_pos, abs_of_pos
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ |z.re| ≤ 1 / 2

Tactic:
hz.2.2.1

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ |z.re| ≤ 1 / 2

Tactic:
exact hz.2.2.1

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
right : z.im ≤ y
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) y 2

Tactic:
rw [sq_le_sq₀ hz.1 (hz.1.trans hz.2.1)]

Premises used: sq_le_sq₀, And.right, And.left, LE.le.trans
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ z.im ≤ y

Tactic:
hz.2.1

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ z.im ≤ y

Tactic:
exact hz.2.1

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
obtain : ∀ (γ : SL(2, ℤ)) (hγ : γ • τ ∈ fd), ∃ (γ : SL(2, ℤ)), 1 / 2 ≤ (γ • τ).im
⊢ ∃ (γ : SL(2, ℤ)), 1 / 2 ≤ (γ • τ).im

Tactic:
obtain ⟨γ, hγ⟩ := exists_smul_mem_fd τ

Premises used: ModularGroup.exists_smul_mem_fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
h : 1 / 2 ≤ (γ • τ).im
⊢ ∃ (γ : SL(2, ℤ)), 1 / 2 ≤ (γ • τ).im

Tactic:
use γ
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
nlinarith : (γ • τ).im < 1 / 2 → 2 / 2 = 1
nlinarith₁ : (γ • τ).im < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : (γ • τ).im < 1 / 2 → GT.gt (α := ℝ) 2 0
nlinarith₃ :
  (γ • τ).im < 1 / 2 →
    3 * (2 * (γ • τ).im - HMul.hMul (α := ℝ) 1 1) + (3 - 4 * HPow.hPow (β := ℕ) (γ • τ).im 2) + 4 * (0 - (γ • τ).im) +
        2 * (0 - (2 * (γ • τ).im - HMul.hMul (α := ℝ) 1 1) * (0 - (γ • τ).im)) =
      0
nlinarith₄ : (γ • τ).im < 1 / 2 → GT.gt (α := ℝ) 3 0
nlinarith₅ : (γ • τ).im < 1 / 2 → GT.gt (α := ℝ) 4 0
nlinarith₆ : (γ • τ).im < 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ 1 / 2 ≤ (γ • τ).im

Tactic:
nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]

Premises used: UpperHalfPlane.im_pos, ModularGroup.three_le_four_mul_im_sq_of_mem_fd, HSMul.hSMul
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
inl :
  ∀ (h : 1 / 2 ≤ τ.im),
    ∃ (γ : SL(2, ℤ)),
      1 / 2 ≤ (γ • τ).im ∧
        ‖denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
              (↑τ : ℂ)‖ ≤
          1
inr :
  ∀ (h : τ.im ≤ 1 / 2),
    ∃ (γ : SL(2, ℤ)),
      1 / 2 ≤ (γ • τ).im ∧
        ‖denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
              (↑τ : ℂ)‖ ≤
          1
⊢ ∃ (γ : SL(2, ℤ)),
    1 / 2 ≤ (γ • τ).im ∧
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖ ≤
        1

Tactic:
rcases le_total (1 / 2) τ.im with h | h

Premises used: HDiv.hDiv, le_total, UpperHalfPlane.im, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) 1))
        (↑τ : ℂ)‖ ≤
    1

Tactic:
simp only [map_one, denom_one, norm_one, le_refl]

Premises used: le_refl, NormOneClass.norm_one, map_one, UpperHalfPlane.denom_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ∃ (γ : SL(2, ℤ)),
    1 / 2 ≤ (γ • τ).im ∧
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖ ≤
        1

Tactic:
exact ⟨1, (one_smul SL(2, ℤ) τ).symm ▸ h, by
      simp only [map_one, denom_one, norm_one, le_refl]⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ (γ : SL(2, ℤ)),
    1 / 2 ≤ (γ • τ).im ∧
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖ ≤
        1

Tactic:
(exists_one_half_le_im_smul τ).imp (fun γ hγ ↦ ⟨hγ, ?_⟩)

Premises used: Exists.imp, ModularGroup.exists_one_half_le_im_smul, And.intro
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ.im ≤ 1 / 2
inr :
  ∀ (γ : SL(2, ℤ)) (hγ : 1 / 2 ≤ (γ • τ).im),
    ‖denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
          (↑τ : ℂ)‖ ≤
      1
⊢ ∃ (γ : SL(2, ℤ)),
    1 / 2 ≤ (γ • τ).im ∧
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖ ≤
        1

Tactic:
refine (exists_one_half_le_im_smul τ).imp (fun γ hγ ↦ ⟨hγ, ?_⟩)

Premises used: Exists.imp, ModularGroup.exists_one_half_le_im_smul
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
⊢ τ.im ≤ (γ • τ).im

Tactic:
have h1 : τ.im ≤ (γ • τ).im := h.trans hγ
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ (γ • τ).im
⊢ τ.im *
      HPow.hPow (β := ℕ)
        ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖
        2 ≤
    τ.im

Tactic:
rw [im_smul_eq_div_normSq, le_div_iff₀ (normSq_denom_pos γ τ.im_ne_zero),
      normSq_eq_norm_sq] at h1

Premises used: Real, UpperHalfPlane.im_ne_zero, Complex.normSq_eq_norm_sq, UpperHalfPlane.normSq_denom_pos, Matrix.SpecialLinearGroup.map, Int.castRingHom, ModularGroup.im_smul_eq_div_normSq, le_div_iff₀, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 :
  τ.im *
      HPow.hPow (β := ℕ)
        ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖
        2 ≤
    τ.im
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑τ : ℂ)‖ ≤
    1

Tactic:
simpa only [sq_le_one_iff_abs_le_one, abs_norm] using
      (mul_le_iff_le_one_right τ.2).mp h1

Premises used: Iff.mp, sq_le_one_iff_abs_le_one, abs_norm, mul_le_iff_le_one_right, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
inst_3 : LinearOrder R
inst_4 : IsOrderedRing R
inst_5 : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
inl :
  ∀ (h : Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)),
    Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1
inr :
  ∀ (h : Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)),
    Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1
⊢ Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1

Tactic:
rcases HasDetPlusMinusOne.det_eq hg with h | h

Premises used: Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
inst_3 : LinearOrder R
inst_4 : IsOrderedRing R
inst_5 : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)
⊢ Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
inst_3 : LinearOrder R
inst_4 : IsOrderedRing R
inst_5 : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)
⊢ Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
inst_3 : LinearOrder R
inst_4 : IsOrderedRing R
⊢ Γ.HasDetPlusMinusOne ↔
    ∀ {g : GL n R}, g ∈ Γ → Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1

Tactic:
⟨fun h {g} hg ↦ h.abs_det hg, fun h ↦ ⟨?_⟩⟩

Premises used: Iff.intro, Subgroup.HasDetPlusMinusOne.mk, Subgroup.HasDetPlusMinusOne.abs_det
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
inst_3 : LinearOrder R
inst_4 : IsOrderedRing R
refine :
  ∀ (h : ∀ {g : GL n R}, g ∈ Γ → Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1)
    {g : GL n R} (hg : g ∈ Γ),
    Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
      Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)
⊢ Γ.HasDetPlusMinusOne ↔
    ∀ {g : GL n R}, g ∈ Γ → Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1

Tactic:
refine ⟨fun h {g} hg ↦ h.abs_det hg, fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
inst_3 : LinearOrder R
inst_4 : IsOrderedRing R
h : ∀ {g : GL n R}, g ∈ Γ → Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1
⊢ ∀ {g : GL n R} (hg : g ∈ Γ),
    Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
      Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)

Tactic:
simpa [-GeneralLinearGroup.val_det_apply, abs_eq zero_le_one] using @h

Premises used: abs_eq, zero_le_one, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ_1 : Subgroup (GL n R)
Γ : Subgroup (SL n R)
g : GL n R
hg : g ∈ map toGL Γ
rcases :
  ∀ (g : SL n R) (hg : g ∈ (↑Γ : Set (SL n R))),
    Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) ((toGL : (a : SL n R) → GL n R) g) : Rˣ)
      (1 : Rˣ)
⊢ Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)

Tactic:
rcases hg with ⟨g, hg, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ_1 : Subgroup (GL n R)
Γ : Subgroup (SL n R)
g : SL n R
hg : g ∈ (↑Γ : Set (SL n R))
⊢ Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) ((toGL : (a : SL n R) → GL n R) g) : Rˣ) (1 : Rˣ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ_1 : Subgroup (GL n R)
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
Γ : Subgroup (SL n R)
g : GL n S
hg : Membership.mem (γ := Subgroup (GL n S)) (map (mapGL S) Γ) g
rcases :
  ∀ (g : SL n R) (hg : g ∈ (↑Γ : Set (SL n R))),
    Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) ((mapGL S : (a : SL n R) → GL n S) g) : Sˣ)
      (1 : Sˣ)
⊢ Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) g : Sˣ) (1 : Sˣ)

Tactic:
rcases hg with ⟨g, hg, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ_1 : Subgroup (GL n R)
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
Γ : Subgroup (SL n R)
g : SL n R
hg : g ∈ (↑Γ : Set (SL n R))
⊢ Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) ((mapGL S : (a : SL n R) → GL n S) g) : Sˣ)
    (1 : Sˣ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
g : GL n S
hg : Membership.mem (γ := Subgroup (GL n S)) (MonoidHom.range (G := SL n R) (mapGL S)) g
rcases :
  ∀ (g : SL n R),
    Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) ((mapGL S : (a : SL n R) → GL n S) g) : Sˣ)
      (1 : Sˣ)
⊢ Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) g : Sˣ) (1 : Sˣ)

Tactic:
rcases hg with ⟨g, hg, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
g : SL n R
⊢ Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) ((mapGL S : (a : SL n R) → GL n S) g) : Sˣ)
    (1 : Sˣ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : CommRing R
Γ : Subgroup (GL n R)
inst_3 : Γ.HasDetOne
g : GL n R
hg : g ∈ Γ
⊢ Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
    Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)

Tactic:
simp [HasDetOne.det_eq hg]

Premises used: Subgroup.HasDetOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
mp : IsArithmetic (map (mapGL ℝ) Γ) → Γ.FiniteIndex
mpr : Γ.FiniteIndex → IsArithmetic (map (mapGL ℝ) Γ)
⊢ IsArithmetic (map (mapGL ℝ) Γ) ↔ Γ.FiniteIndex

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
⊢ IsArithmetic (map (mapGL ℝ) Γ) → Γ.FiniteIndex

Tactic:
fun ⟨h⟩ ↦ ⟨?_⟩

Premises used: Subgroup.FiniteIndex, _private.0.Subgroup.isArithmetic_iff_finiteIndex.match_1, Subgroup.FiniteIndex.mk
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
mp :
  IsArithmetic (map (mapGL ℝ) Γ) →
    ∀ (h : Commensurable (G := GL (Fin 2) ℝ) (map (mapGL ℝ) Γ) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))), Γ.index ≠ 0
⊢ IsArithmetic (map (mapGL ℝ) Γ) → Γ.FiniteIndex

Tactic:
refine fun ⟨h⟩ ↦ ⟨?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
h_1 : IsArithmetic (map (mapGL ℝ) Γ)
h : Commensurable (G := GL (Fin 2) ℝ) (map (mapGL ℝ) Γ) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ Γ.index ≠ 0

Tactic:
simpa [Commensurable, MonoidHom.range_eq_map, ← relIndex_comap,
      comap_map_eq_self_of_injective mapGL_injective] using h

Premises used: MonoidHom.range_eq_map, Matrix.SpecialLinearGroup.mapGL_injective, Subgroup.comap_map_eq_self_of_injective, Subgroup.Commensurable, Subgroup.relIndex_comap
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
⊢ Γ.FiniteIndex → IsArithmetic (map (mapGL ℝ) Γ)

Tactic:
fun ⟨h⟩ ↦ ⟨?_⟩

Premises used: Subgroup.IsArithmetic.mk, Real, Subgroup.map, _private.0.Subgroup.isArithmetic_iff_finiteIndex.match_2, Subgroup.IsArithmetic, Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
mpr :
  Γ.FiniteIndex →
    ∀ (h : Γ.index ≠ 0), Commensurable (G := GL (Fin 2) ℝ) (map (mapGL ℝ) Γ) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ Γ.FiniteIndex → IsArithmetic (map (mapGL ℝ) Γ)

Tactic:
refine fun ⟨h⟩ ↦ ⟨?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
h_1 : Γ.FiniteIndex
h : Γ.index ≠ 0
⊢ Commensurable (G := GL (Fin 2) ℝ) (map (mapGL ℝ) Γ) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
simpa [Commensurable, MonoidHom.range_eq_map, ← relIndex_comap,
      comap_map_eq_self_of_injective mapGL_injective] using h

Premises used: MonoidHom.range_eq_map, Matrix.SpecialLinearGroup.mapGL_injective, Subgroup.comap_map_eq_self_of_injective, Subgroup.Commensurable, Subgroup.relIndex_comap
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ : Subgroup SL(2, ℤ)
inst_2 : Γ.FiniteIndex
⊢ IsArithmetic (map (mapGL ℝ) Γ)

Tactic:
isArithmetic_iff_finiteIndex.mpr ‹_›

Premises used: Iff.mpr, Subgroup.isArithmetic_iff_finiteIndex