awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₇ : HVAdd.hVAdd (α := ℝ) (-1) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₈ : ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₇ : HVAdd.hVAdd (α := ℝ) (-1) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₈ : ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₉ : S⁻¹ • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₇ : HVAdd.hVAdd (α := ℝ) (-1) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₈ : ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₉ : S⁻¹ • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₁₀ : -S • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₇ : HVAdd.hVAdd (α := ℝ) (-1) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₈ : ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₉ : S⁻¹ • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁₀ : -S • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₁₁ : S • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₇ : HVAdd.hVAdd (α := ℝ) (-1) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₈ : ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₉ : S⁻¹ • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁₀ : -S • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁₁ : S • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₁₂ : T • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this : S • ρ = T • ρ
rw : S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁ : -S • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₂ : S⁻¹ • T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₃ : T⁻¹ • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₄ : HPow.hPow (β := ℤ) T (-1) • HVAdd.hVAdd (α := ℝ) 1 ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₅ : HVAdd.hVAdd (α := ℝ) (↑(-1) : ℝ) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₆ : HVAdd.hVAdd (α := ℝ) (-(↑1 : ℝ)) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₇ : HVAdd.hVAdd (α := ℝ) (-1) (HVAdd.hVAdd (α := ℝ) 1 ρ) = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₈ : ρ = S • HVAdd.hVAdd (α := ℝ) 1 ρ
rw₉ : S⁻¹ • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁₀ : -S • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁₁ : S • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
rw₁₂ : T • ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
have rw₁₃ : HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this : S • ρ = T • ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
have this₁ : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
Tactic: have : (S * T⁻¹) • ((1 : ℝ) +ᵥ ρ) = (1 : ℝ) +ᵥ ρ := by
    rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
have hg₁ : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
Tactic: rw [this] at hg
Cleared hypotheses: hg, hg', hc, hd, this_1, hgeq, hnorm, this_2, h, h', hρ, this_3, this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
have rw : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
  T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
Tactic: rw [hgeq]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this_4 : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
have inl : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
  T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this_4 : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
inl :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0),
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
      T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
have inr : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1),
  T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = S * T⁻¹ ∨
    T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
have suffices : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
Tactic: suffices g 0 0 = 0 ∨ g 0 0 = -1 by rcases this with h | h <;> simp [h]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
have this₁ : LE.le (α := ℝ) (-1) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0
Tactic: have : (-1 : ℝ) ≤ g 0 0 ∧ g 0 0 ≤ 0 := by
    simpa only [ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, coe_vadd, add_re, ofReal_re,
      show 1 + (-2⁻¹ : ℝ) = 2⁻¹ by norm_num, intCast_re, abs_le, ← sub_le_iff_le_add',
      show (-2⁻¹ : ℝ) - (2⁻¹ : ℝ) = -1 by norm_num, add_le_iff_nonpos_right, Int.cast_nonpos] using
      hg.2
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 • HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟
hg' :
  ‖denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
        (↑z : ℂ)‖ ≤
    1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1
hd : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 - 1
hgeq : g = T ^ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * S * T⁻¹
hnorm : HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1) ≤ 1
this_2 :
  (normSq : (a : ℂ) → ℝ) ((↑z : ℂ) - 1) = HAdd.hAdd (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (-2 * z.re + 1)
h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
h' : z.re = 1 / 2
hρ : z = HVAdd.hVAdd (α := ℝ) 1 ρ
this_3 : S • ρ = T • ρ
this_4 : (S * T⁻¹) • HVAdd.hVAdd (α := ℝ) 1 ρ = HVAdd.hVAdd (α := ℝ) 1 ρ
this : LE.le (α := ℝ) (-1) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℝ) ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 0 ∨ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1
have this₁ : -1 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0
Tactic: rw [← Int.cast_one, ← Int.cast_neg, Int.cast_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
⊢ (g • z).im = z.im
have inr : ∀ (this : ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im), (g • z).im = z.im)
  (hden : ¬z.im ≤ (g • z).im), (g • z).im = z.im
Tactic: wlog hden : z.im ≤ (g • z).im
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
inr :
  ∀ (this : ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im), (g • z).im = z.im)
    (hden : ¬z.im ≤ (g • z).im), (g • z).im = z.im
⊢ (g • z).im = z.im
have wlog : ∀ {g : SL(2, ℤ)} {z : ℍ} (hz : z ∈ 𝒟) (hg : g • z ∈ 𝒟) (hden : z.im ≤ (g • z).im), (g • z).im = z.im
Tactic: wlog hden : z.im ≤ (g • z).im
Cleared hypotheses: hz, hg