-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
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) : ℂ)
⊢ (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑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) : ℂ) /
          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) :
              ℂ) *
        (HPow.hPow (β := ℤ)
            (denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)) 2)⁻¹ +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)
have h : (↑(((↑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: rw [(by intros; field_simp : ∀ {a b c d f e : ℂ} (he : e ≠ 0), a / b =
    c / d * (e ^ (2 : ℤ))⁻¹ + f / e ↔ a * e ^ 2 / b = c / d + e * f) (denom_ne_zero B z)]