-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0
c : ℝ := (↑c' : ℝ)
hc : c ≠ 0
h₁ :
  HMul.hMul (α := ℝ) 3 3 * HPow.hPow (β := ℕ) c 4 ≤
    4 * HPow.hPow (β := ℕ) (g • z).im 2 * (4 * HPow.hPow (β := ℕ) z.im 2) * HPow.hPow (β := ℕ) c 4
h₂ :
  HPow.hPow (β := ℕ) (c * z.im) 4 /
      HPow.hPow (α := ℝ) (β := ℕ)
        ((normSq : (a : ℂ) → ℝ)
            (denom
              ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
              (↑z : ℂ)) :
          ℝ)
        2 ≤
    1
linarith :
  16 <
      HPow.hPow (β := ℕ) (c * z.im) 4 /
          HPow.hPow (α := ℝ) (β := ℕ)
            ((normSq : (a : ℂ) → ℝ)
                (denom
                  ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                    ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                  (↑z : ℂ)) :
              ℝ)
            2 *
        16 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ :
  16 <
      HPow.hPow (β := ℕ) (c * z.im) 4 /
          HPow.hPow (α := ℝ) (β := ℕ)
            ((normSq : (a : ℂ) → ℝ)
                (denom
                  ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                    ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                  (↑z : ℂ)) :
              ℝ)
            2 *
        16 →
    16 *
          (1 *
              (HPow.hPow (β := ℕ) (c * z.im) 4 /
                HPow.hPow (α := ℝ) (β := ℕ)
                  ((normSq : (a : ℂ) → ℝ)
                      (denom
                        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                        (↑z : ℂ)) :
                    ℝ)
                  2) -
            HMul.hMul (α := ℝ) 1 1) +
        (HMul.hMul (α := ℝ) 1 16 -
          1 *
              (HPow.hPow (β := ℕ) (c * z.im) 4 /
                HPow.hPow (α := ℝ) (β := ℕ)
                  ((normSq : (a : ℂ) → ℝ)
                      (denom
                        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                        (↑z : ℂ)) :
                    ℝ)
                  2) *
            HMul.hMul (α := ℝ) 1 16) =
      0
⊢ HPow.hPow (β := ℕ) (c * z.im) 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16 ≤
    16
have linarith₂ : 16 <
    HPow.hPow (β := ℕ) (c * z.im) 4 /
        HPow.hPow (α := ℝ) (β := ℕ)
          ((normSq : (a : ℂ) → ℝ)
              (denom
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                  ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
                (↑z : ℂ)) :
            ℝ)
          2 *
      16 →
  GT.gt (α := ℝ) 16 0
Tactic: linarith