awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y ↔
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
have h : z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y →
  Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
h :
  z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y →
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y ↔
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
have h₁ : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z →
  z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ 0 < z.im
have apply : 0 ≠ z.im
Tactic: apply hz.lt_of_ne
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ 0 ≠ z.im
have contrapose! : ∀ (h3 : 0 = z.im), ‖z‖ < 1
Tactic: contrapose! h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
have hz' : 0 < z.im
Tactic: have hz' : 0 < z.im := by
      apply hz.lt_of_ne
      contrapose! h3
      simpa [← sq_lt_one_iff₀ (norm_nonneg _), ← Complex.normSq_eq_norm_sq, Complex.normSq,
        ← h3, ← sq] using h2.trans_lt (by norm_num)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
⊢ IsCompact (truncatedFundamentalDomain y)
have 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‖}
Tactic: rw [isEmbedding_coe.isCompact_iff, coe_truncatedFundamentalDomain,
    Metric.isCompact_iff_isClosed_bounded]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
⊢ 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‖}
have left : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
left : IsClosed (X := ℂ) {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‖}
have right : Bornology.IsBounded (α := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
have left : IsClosed (X := ℂ) fun (z : ℂ) ↦ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖
Tactic: apply (isClosed_le continuous_const Complex.continuous_im).inter
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖
have left : IsClosed (X := ℂ) fun (z : ℂ) ↦ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖
Tactic: apply (isClosed_le Complex.continuous_im continuous_const).inter
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖
have left : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖
Tactic: apply (isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const).inter
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
⊢ Bornology.IsBounded (α := ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
have 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
Tactic: refine (Metric.isBounded_iff_subset_closedBall 0).mpr ⟨√((1 / 2) ^ 2 + y ^ 2), fun z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
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
have right : ‖z‖ ≤ √(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)
Tactic: simp only [mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ ‖z‖ ≤ √(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)
have right : HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)) 2
Tactic: refine le_of_sq_le_sq ?_ (by positivity)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 ≤ HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2)) 2
have right : HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2
Tactic: rw [Real.sq_sqrt (by positivity), Complex.norm_eq_sqrt_sq_add_sq, Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2
have right : HPow.hPow (β := ℕ) z.re 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2 + HPow.hPow (β := ℕ) y 2
have right₁ : HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) y 2
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ HPow.hPow (β := ℕ) z.re 2 ≤ HPow.hPow (β := ℕ) (1 / 2) 2
have right : |z.re| ≤ 1 / 2
Tactic: rw [sq_le_sq, abs_of_pos <| one_half_pos (α := ℝ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
y : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) y 2
have right : z.im ≤ y
Tactic: rw [sq_le_sq₀ hz.1 (hz.1.trans hz.2.1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
⊢ ∃ (γ : SL(2, ℤ)), 1 / 2 ≤ (γ • τ).im
have obtain : ∀ (γ : SL(2, ℤ)) (hγ : γ • τ ∈ fd), ∃ (γ : SL(2, ℤ)), 1 / 2 ≤ (γ • τ).im
Tactic: obtain ⟨γ, hγ⟩ := exists_smul_mem_fd τ
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
⊢ ∃ (γ : SL(2, ℤ)), 1 / 2 ≤ (γ • τ).im
have h : 1 / 2 ≤ (γ • τ).im
Tactic: use γ
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
⊢ 1 / 2 ≤ (γ • τ).im
have nlinarith : (γ • τ).im < 1 / 2 → 2 / 2 = 1
Tactic: nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
nlinarith : (γ • τ).im < 1 / 2 → 2 / 2 = 1
⊢ 1 / 2 ≤ (γ • τ).im
have nlinarith₁ : (γ • τ).im < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
nlinarith : (γ • τ).im < 1 / 2 → 2 / 2 = 1
nlinarith₁ : (γ • τ).im < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 / 2 ≤ (γ • τ).im
have nlinarith₂ : (γ • τ).im < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 1 / 2 ≤ (γ • τ).im
have 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
Tactic: nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 1 / 2 ≤ (γ • τ).im
have nlinarith₄ : (γ • τ).im < 1 / 2 → GT.gt (α := ℝ) 3 0
Tactic: nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 1 / 2 ≤ (γ • τ).im
have nlinarith₅ : (γ • τ).im < 1 / 2 → GT.gt (α := ℝ) 4 0
Tactic: nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
τ : ℍ
⊢ ∃ (γ : SL(2, ℤ)),
    1 / 2 ≤ (γ • τ).im ∧
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖ ≤
        1
have 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
Tactic: rcases le_total (1 / 2) τ.im with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ ∃ (γ : SL(2, ℤ)),
    1 / 2 ≤ (γ • τ).im ∧
      ‖denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑τ : ℂ)‖ ≤
        1
have 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
Tactic: rcases le_total (1 / 2) τ.im with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have 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
Tactic: refine (exists_one_half_le_im_smul τ).imp (fun γ hγ ↦ ⟨hγ, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑τ : ℂ)‖ ≤
    1
have h1 : τ.im ≤ (γ • τ).im
Tactic: have h1 : τ.im ≤ (γ • τ).im := h.trans hγ
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ (γ • τ).im
⊢ ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑τ : ℂ)‖ ≤
    1
have h1₁ : τ.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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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 ∈ Γ
⊢ Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1
have 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
Tactic: rcases HasDetPlusMinusOne.det_eq hg with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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
⊢ Eq.{u_2 + 1} (α := R) |(↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R)| 1
have 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
Tactic: rcases HasDetPlusMinusOne.det_eq hg with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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
have 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ˣ)
Tactic: refine ⟨fun h {g} hg ↦ h.abs_det hg, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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 Γ
⊢ Eq.{u_2 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)
have 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ˣ)
Tactic: rcases hg with ⟨g, hg, rfl⟩
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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
⊢ Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) g : Sˣ) (1 : Sˣ)
have 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ˣ)
Tactic: rcases hg with ⟨g, hg, rfl⟩
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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
⊢ Eq.{u_3 + 1} (α := Sˣ) ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) g : Sˣ) (1 : Sˣ)
have 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ˣ)
Tactic: rcases hg with ⟨g, hg, rfl⟩
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
⊢ IsArithmetic (map (mapGL ℝ) Γ) ↔ Γ.FiniteIndex
have mp : IsArithmetic (map (mapGL ℝ) Γ) → Γ.FiniteIndex
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
mp : IsArithmetic (map (mapGL ℝ) Γ) → Γ.FiniteIndex
⊢ IsArithmetic (map (mapGL ℝ) Γ) ↔ Γ.FiniteIndex
have mpr : Γ.FiniteIndex → IsArithmetic (map (mapGL ℝ) Γ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
⊢ IsArithmetic (map (mapGL ℝ) Γ) → Γ.FiniteIndex
have mp : IsArithmetic (map (mapGL ℝ) Γ) →
  ∀ (h : Commensurable (G := GL (Fin 2) ℝ) (map (mapGL ℝ) Γ) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))), Γ.index ≠ 0
Tactic: refine fun ⟨h⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
⊢ Γ.FiniteIndex → IsArithmetic (map (mapGL ℝ) Γ)
have mpr : Γ.FiniteIndex →
  ∀ (h : Γ.index ≠ 0), Commensurable (G := GL (Fin 2) ℝ) (map (mapGL ℝ) Γ) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
Tactic: refine fun ⟨h⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
⊢ Γ.HasDetPlusMinusOne
have rw : ∀ {g : GL (Fin 2) ℝ}, g ∈ Γ → Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1
Tactic: rw [hasDetPlusMinusOne_iff_abs_det]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
⊢ Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1
have obtain : ∀ (n : ℕ) (hn : 0 < n),
  n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ →
    ∀ (hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ),
      Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1
Tactic: obtain ⟨n, hn, _, hgn⟩ := Subgroup.exists_pow_mem_of_relIndex_ne_zero
    Subgroup.IsArithmetic.is_commensurable.2 hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
⊢ Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1
have suffices : |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
Tactic: suffices |(g.det ^ n).val| = 1 by simpa [← abs_pow, abs_pow_eq_one _ (Nat.ne_zero_of_lt hn)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
⊢ |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
have obtain : ∀ (t : SL(2, ℤ)) (ht : (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t = g ^ n),
  |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
Tactic: obtain ⟨t, ht⟩ := hgn.1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t = g ^ n
⊢ |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
have this : Eq (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (g ^ n) : ℝˣ)
  ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t) : ℝˣ)
Tactic: have := congr_arg Matrix.GeneralLinearGroup.det ht.symm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t = g ^ n
this :
  Eq (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (g ^ n) : ℝˣ)
    ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t) : ℝˣ)
⊢ |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
have this₁ : HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n = 1
Tactic: rw [Matrix.SpecialLinearGroup.det_mapGL, map_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
⊢ (Γ ⊓ Γ').IsArithmetic
have is_commensurable : (Γ ⊓ Γ').Commensurable (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
⊢ (Γ ⊓ Γ').Commensurable (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
have is_commensurable : (Γ ⊓ Γ').relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
Tactic: constructor