-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
A B : SL(2, ℤ)
z : ℍ
h0 :
  ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 0 0 =
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ∧
    ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 0 1 =
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1 +
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ∧
      ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0 =
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
            (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ∧
        ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 1 =
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1 +
            (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1
⊢ (↑((↑(A * B) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
      denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) B))
        (↑z : ℂ) =
    HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑(↑B : Matrix (Fin 2) (Fin 2) ℤ).det : ℂ) +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        denom
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) B) :
              GL (Fin 2) ℝ))
          (↑z : ℂ)
have simp : (HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) +
      HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) *
    ((↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) =
  (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
      (HMul.hMul (α := ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) -
        HMul.hMul (α := ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) +
    (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
      ((HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) +
            HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)
              (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) *
          (↑z : ℂ) +
        (HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ) +
          HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)))
Tactic: simp only [Fin.isValue, coe_mul, h0.2.2.1, Int.cast_add, Int.cast_mul, ModularGroup.denom_apply,
    Matrix.det_fin_two B.1, Int.cast_sub, ← map_mul, h0.2.2.2]