-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
z : ℍ
hd :
  (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) *
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) -
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        denom
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A) : GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ))
          (↑z : ℂ) =
    (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
this :
  denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
      (num ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) /
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)) =
    denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A)) (↑(B • z) : ℂ)
h :
  (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) *
          denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) *
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) /
      (denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
          (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
            ℂ) *
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)) =
    ((↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) *
            denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) -
          (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
              denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
                (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
                  ℂ) *
            denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)) /
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
          (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
            ℂ) +
      denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) *
        (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
⊢ (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) *
        HPow.hPow (β := ℕ) (denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ))
          2 /
      denom
        (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A) : GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ))
        (↑z : ℂ) =
    (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
          (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
            ℂ) +
      denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) *
        (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)

Tactic:
simp only [pow_two, ← mul_assoc, denom_cocycle A B z.im_ne_zero, this,
    ModularGroup.sl_moeb, ← hd]

Premises used: Real, UpperHalfPlane.im_ne_zero, pow_two, ModularGroup.sl_moeb, mul_assoc, UpperHalfPlane.denom_cocycle, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL