-- 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 ((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) : ℂ)
have h : (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) =
  (↑(((↑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, ℝ)) A))
          (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) 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) :
          ℂ) *
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
Tactic: field_simp [denom_ne_zero A (toGL (φ B) • z)]